Theorem pm4.71i 559

Description: Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Hypothesis

Ref	Expression
pm4.71i.1	⊢ (𝜑 → 𝜓)

Assertion

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

Proof of Theorem pm4.71i

Step	Hyp	Ref	Expression
1		pm4.71i.1	. 2 ⊢ (𝜑 → 𝜓)
2		pm4.71 557	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 230	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.71ri  560  pm4.24  563  anabs1  663  pm4.45im  828  pm4.45  1000  eu6lem  2574  2eu5  2657  dfid2  5522  imadmrn  6030  dff1o2  6780  f12dfv  7222  isof1oidb  7273  isof1oopb  7274  xpsnen  8993  dfac5lem2  10040  axgroth6  10745  eqreznegel  12878  xrnemnf  13062  xrnepnf  13063  dfrp2  13341  elioopnf  13390  elioomnf  13391  elicopnf  13392  elxrge0  13404  isprm2  16645  efgrelexlemb  19719  opsrtoslem1  22046  tgphaus  24095  cfilucfil3  25300  ioombl1lem4  25541  vitalilem1  25588  ellogdm  26619  nb3grpr2  29469  upgr2wlk  29753  erclwwlkref  30108  erclwwlknref  30157  0spth  30214  0crct  30221  pjimai  32265  eulerpartlemt0  34532  bnj1101  34946  satfvsuclem2  35561  bj-snglc  37295  bj-epelb  37395  bj-opelidb1  37486  icorempo  37684  wl-cases2-dnf  37854  matunitlindf  37956  disjressuc2  38749  dflim5  43778  pm11.58  44838