Theorem pm4.71ri 637

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

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. 2 |- ( ph -> ps )
2		pm4.71r 635	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )
3	1, 2	mpbi 211	1 |- ( ph <-> ( ps /\ ph ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 188  df-an 372

This theorem is referenced by:  biadan2  646  anabs7  817  orabs  863  prlem2  971  eu5  2302  2moswap  2353  exsnrex  3980  eliunxp  4934  asymref  5178  dffun9  5572  funcnv  5604  funcnv3  5605  f1ompt  6003  eufnfv  6098  dff1o6  6133  dfom2  6652  elxp4  6695  elxp5  6696  abexex  6734  dfoprab4  6808  tpostpos  6948  brwitnlem  7164  erovlem  7414  elixp2  7481  xpsnen  7609  elom3  8106  cardval2  8377  isinfcard  8474  infmap2  8599  elznn0nn  10902  zrevaddcl  10933  qrevaddcl  11237  hash2prb  12581  cotr2g  12984  climreu  13563  isprm3  14576  hashbc0  14900  imasleval  15390  isssc  15668  isgim  16869  eldprd  17579  brric2  17916  islmim  18228  tgval2  19913  eltg2b  19916  snfil  20821  isms2  21407  setsms  21437  elii1  21905  phtpcer  21968  elovolm  22370  ellimc2  22774  limcun  22792  1cubr  23710  fsumvma2  24084  dchrelbas3  24108  rusgranumwlks  25626  isgrpo  25866  issubgo  25973  ismgmOLD  25990  mdsl2i  27917  cvmdi  27919  rabfmpunirn  28198  eulerpartlemn  29166  bnj580  29676  bnj1049  29735  snmlval  30006  elmthm  30166  brtxp2  30597  brpprod3a  30602  prtlem100  32338  islln2  32988  islpln2  33013  islvol2  33057  elmapintrab  36095  clcnvlem  36143  eliunxp2  39718  elbigo  39965