Theorem pm4.71i 567

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 565	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 232	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:  pm4.71ri  568  pm4.24  571  anabs1  672  pm4.45im  838  pm4.45  1011  eu6lem  2600  2eu5  2682  dfid2  5544  imadmrn  6059  dff1o2  6812  f12dfv  7257  isof1oidb  7308  isof1oopb  7309  xpsnen  9033  dfac5lem2  10080  axgroth6  10786  eqreznegel  12935  xrnemnf  13119  xrnepnf  13120  dfrp2  13398  elioopnf  13447  elioomnf  13448  elicopnf  13449  elxrge0  13461  isprm2  16716  efgrelexlemb  19790  opsrtoslem1  22105  tgphaus  24174  cfilucfil3  25379  ioombl1lem4  25620  vitalilem1  25667  ellogdm  26701  nb3grpr2  29581  upgr2wlk  29864  erclwwlkref  30219  erclwwlknref  30268  0spth  30325  0crct  30332  pjimai  32376  eulerpartlemt0  34663  bnj1101  35077  satfvsuclem2  35707  bj-snglc  37451  bj-epelb  37551  bj-opelidb1  37642  icorempo  37842  wl-cases2-dnf  38012  matunitlindf  38114  disjressuc2  38907  dflim5  43903  pm11.58  44963