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  662  pm4.45im  827  pm4.45  999  eu6lem  2566  2eu5  2649  rabeqcOLD  3654  dfid2  5528  imadmrn  6030  dff1o2  6787  f12dfv  7230  isof1oidb  7281  isof1oopb  7282  xpsnen  9002  dfac5lem2  10053  axgroth6  10757  eqreznegel  12869  xrnemnf  13053  xrnepnf  13054  dfrp2  13331  elioopnf  13380  elioomnf  13381  elicopnf  13382  elxrge0  13394  isprm2  16628  efgrelexlemb  19664  opsrtoslem1  21995  tgphaus  24037  cfilucfil3  25253  ioombl1lem4  25495  vitalilem1  25542  ellogdm  26581  nb3grpr2  29363  upgr2wlk  29647  erclwwlkref  29999  erclwwlknref  30048  0spth  30105  0crct  30112  pjimai  32155  eulerpartlemt0  34353  bnj1101  34767  satfvsuclem2  35340  bj-snglc  36950  bj-epelb  37050  bj-opelidb1  37134  icorempo  37332  wl-cases2-dnf  37493  matunitlindf  37605  disjressuc2  38367  dflim5  43311  pm11.58  44372