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  2567  2eu5  2650  rabeqcOLD  3660  dfid2  5538  imadmrn  6044  dff1o2  6808  f12dfv  7251  isof1oidb  7302  isof1oopb  7303  xpsnen  9029  dfac5lem2  10084  axgroth6  10788  eqreznegel  12900  xrnemnf  13084  xrnepnf  13085  dfrp2  13362  elioopnf  13411  elioomnf  13412  elicopnf  13413  elxrge0  13425  isprm2  16659  efgrelexlemb  19687  opsrtoslem1  21969  tgphaus  24011  cfilucfil3  25227  ioombl1lem4  25469  vitalilem1  25516  ellogdm  26555  nb3grpr2  29317  upgr2wlk  29603  erclwwlkref  29956  erclwwlknref  30005  0spth  30062  0crct  30069  pjimai  32112  eulerpartlemt0  34367  bnj1101  34781  satfvsuclem2  35354  bj-snglc  36964  bj-epelb  37064  bj-opelidb1  37148  icorempo  37346  wl-cases2-dnf  37507  matunitlindf  37619  disjressuc2  38381  dflim5  43325  pm11.58  44386