Theorem pm4.71ri 570

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	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
pm4.71ri	⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Proof of Theorem pm4.71ri

Step	Hyp	Ref	Expression
1		pm4.71ri.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	pm4.71i 569	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 468	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anabs7  677  biadaniALT  833  orabs  1014  prlem2  1071  dfeumo  2562  dfeu  2621  2moswapv  2655  2moswap  2670  exsnrex  4641  eliunxp  5814  asymref  6110  imaindm  6302  dffun9  6569  funcnv  6609  funcnv3  6610  f1ompt  7111  eufnfv  7235  dff1o6  7283  dfom2  7879  elxp4  7934  elxp5  7935  abexex  7983  dfoprab4  8066  tpostpos  8263  brwitnlem  8515  erovlem  8834  elixp2  8929  xpsnen  9080  elom3  9649  ttrclse  9728  cardval2  10072  isinfcard  10171  infmap2  10295  elznn0nn  12707  zrevaddcl  12741  qrevaddcl  13099  hash2prb  14617  hash3tpb  14640  cotr2g  15129  climreu  15723  isprm3  16858  hashbc0  17183  imasleval  17713  xpscf  17737  isssc  17995  issubmndb  19000  isgim  19476  eldprd  20220  isbrric2  20753  islmim  21337  tgval2  23274  eltg2b  23277  snfil  24183  isms2  24769  setsms  24799  elii1  25256  phtpcer  25316  elovolm  25796  ellimc2  26197  limcun  26215  1cubr  27170  fsumvma2  27541  dchrelbas3  27565  2lgslem1b  27719  dmcuts  28177  madeval2  28219  made0  28249  nbgrel  29921  rusgrnumwwlks  30566  isgrpo  31099  mdsl2i  32924  cvmdi  32926  rabfmpunirn  33247  zarcls  34506  eulerpartlemn  35013  bnj580  35543  bnj1049  35604  snmlval  36096  satf0suclem  36140  fmlasuc0  36149  elmthm  36341  brtxp2  36643  brpprod3a  36648  bj-elid6  38091  ismgmOLD  38784  brres2  39205  ralmo  39292  brxrn2  39316  dfsuccl4  39406  redundpim3  39646  prtlem100  39916  islln2  40568  islpln2  40593  islvol2  40637  prjspeclsp  43640  onsucrn  44272  dflim5  44330  en2pr  44547  pren2  44553  elmapintrab  44576  clcnvlem  44622  sprvalpw  48561  sprvalpwn0  48564  prprvalpw  48596  clnbgrel  48925  eliunxp2  49445  elbigo  49662