Theorem pm4.71ri 568

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 567	. 2 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))
3	2	biancomi 466	1 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜑))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anabs7  674  biadaniALT  830  orabs  1012  prlem2  1067  dfeumo  2563  dfeu  2622  2moswapv  2656  2moswap  2671  exsnrex  4639  eliunxp  5809  asymref  6103  imaindm  6286  dffun9  6550  funcnv  6590  funcnv3  6591  f1ompt  7092  eufnfv  7213  dff1o6  7259  dfom2  7848  elxp4  7903  elxp5  7904  abexex  7952  dfoprab4  8036  tpostpos  8226  brwitnlem  8476  erovlem  8795  elixp2  8883  xpsnen  9033  elom3  9603  ttrclse  9682  cardval2  9949  isinfcard  10048  infmap2  10173  elznn0nn  12582  zrevaddcl  12616  qrevaddcl  12972  hash2prb  14485  hash3tpb  14508  cotr2g  14989  climreu  15583  isprm3  16717  hashbc0  17041  imasleval  17571  xpscf  17595  isssc  17853  issubmndb  18839  isgim  19302  eldprd  20046  brric2  20556  islmim  21129  tgval2  23016  eltg2b  23019  snfil  23924  isms2  24510  setsms  24540  elii1  24997  phtpcer  25057  elovolm  25537  ellimc2  25939  limcun  25957  1cubr  26907  fsumvma2  27278  dchrelbas3  27302  2lgslem1b  27456  dmcuts  27884  madeval2  27926  made0  27956  nbgrel  29541  rusgrnumwwlks  30177  isgrpo  30700  mdsl2i  32525  cvmdi  32527  rabfmpunirn  32855  zarcls  34171  eulerpartlemn  34678  bnj580  35208  bnj1049  35269  snmlval  35681  satf0suclem  35725  fmlasuc0  35734  elmthm  35926  brtxp2  36229  brpprod3a  36234  bj-elid6  37662  ismgmOLD  38349  brres2  38772  ralmo  38859  brxrn2  38883  dfsuccl4  38973  redundpim3  39213  prtlem100  39483  islln2  40135  islpln2  40160  islvol2  40204  prjspeclsp  43194  onsucrn  43848  dflim5  43906  en2pr  44123  pren2  44129  elmapintrab  44152  clcnvlem  44199  sprvalpw  48086  sprvalpwn0  48089  prprvalpw  48121  clnbgrel  48450  eliunxp2  48956  elbigo  49173