MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.71ri Unicode version

Theorem pm4.71ri 615
Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)
Hypothesis
Ref Expression
pm4.71ri.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
pm4.71ri  |-  ( ph  <->  ( ps  /\  ph )
)

Proof of Theorem pm4.71ri
StepHypRef Expression
1 pm4.71ri.1 . 2  |-  ( ph  ->  ps )
2 pm4.71r 613 . 2  |-  ( (
ph  ->  ps )  <->  ( ph  <->  ( ps  /\  ph )
) )
31, 2mpbi 200 1  |-  ( ph  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biadan2  624  anabs7  786  orabs  829  prlem2  930  sb6  2148  2moswap  2329  exsnrex  3808  dfom2  4806  eliunxp  4971  asymref  5209  elxp4  5316  elxp5  5317  dffun9  5440  funcnv  5470  funcnv3  5471  f1ompt  5850  eufnfv  5931  abexex  5962  dff1o6  5972  dfoprab4  6363  tpostpos  6458  brwitnlem  6710  erovlem  6959  elixp2  7025  xpsnen  7151  elom3  7559  cardval2  7834  isinfcard  7929  infmap2  8054  elznn0nn  10251  zrevaddcl  10277  qrevaddcl  10552  climreu  12305  isprm3  13043  hashbc0  13328  imasleval  13721  isssc  13975  isgim  15004  eldprd  15517  islmim  16089  tgval2  16976  eltg2b  16979  snfil  17849  isms2  18433  setsms  18463  elii1  18913  phtpcer  18973  elovolm  19324  ellimc2  19717  limcun  19735  1cubr  20635  fsumvma2  20951  dchrelbas3  20975  isgrpo  21737  issubgo  21844  ismgm  21861  mdsl2i  23778  cvmdi  23780  rabfmpunirn  24018  snmlval  24971  brtxp2  25635  brpprod3a  25640  prtlem100  26594  bnj580  28990  bnj1049  29049  sb6NEW7  29298  islln2  29993  islpln2  30018  islvol2  30062
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator