Theorem pm4.71ri 633

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 631	. 2 |- ( ( ph -> ps ) <-> ( ph <-> ( ps /\ ph ) ) )
3	1, 2	mpbi 208	1 |- ( ph <-> ( ps /\ ph ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  biadan2  642  anabs7  808  orabs  852  prlem2  956  sb6OLD  2151  eu5  2300  2moswap  2373  exsnrex  4060  eliunxp  5133  asymref  5376  dffun9  5609  funcnv  5641  funcnv3  5642  f1ompt  6036  eufnfv  6127  dff1o6  6162  dfom2  6675  elxp4  6720  elxp5  6721  abexex  6759  dfoprab4  6833  tpostpos  6967  brwitnlem  7149  erovlem  7399  elixp2  7465  xpsnen  7593  elom3  8056  cardval2  8363  isinfcard  8464  infmap2  8589  elznn0nn  10869  zrevaddcl  10899  qrevaddcl  11195  climreu  13330  isprm3  14076  hashbc0  14373  imasleval  14787  isssc  15041  isgim  16100  eldprd  16821  eldprdOLD  16823  brric2  17172  islmim  17486  tgval2  19219  eltg2b  19222  snfil  20095  isms2  20683  setsms  20713  elii1  21165  phtpcer  21225  elovolm  21616  ellimc2  22011  limcun  22029  1cubr  22896  fsumvma2  23212  dchrelbas3  23236  rusgranumwlks  24620  isgrpo  24862  issubgo  24969  ismgm  24986  mdsl2i  26905  cvmdi  26907  rabfmpunirn  27151  eulerpartlemn  27948  snmlval  28404  brtxp2  29096  brpprod3a  29101  prtlem100  30189  eliunxp2  31864  bnj580  32927  bnj1049  32986  islln2  34184  islpln2  34209  islvol2  34253