Theorem pm4.71i 568

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 566	. 2 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 ↔ (𝜑 ∧ 𝜓)))
3	1, 2	mpbi 233	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜓))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm4.71ri  569  pm4.24  573  anabs1  674  pm4.45im  840  pm4.45  1013  eu6lem  2607  2eu5  2689  dfid2  5559  imadmrn  6073  dff1o2  6827  f12dfv  7272  isof1oidb  7323  isof1oopb  7324  xpsnen  9048  dfac5lem2  10107  axgroth6  10812  eqreznegel  12957  xrnemnf  13141  xrnepnf  13142  dfrp2  13420  elioopnf  13469  elioomnf  13470  elicopnf  13471  elxrge0  13483  isprm2  16739  efgrelexlemb  19819  opsrtoslem1  22174  tgphaus  24242  cfilucfil3  25447  ioombl1lem4  25688  vitalilem1  25735  ellogdm  26769  nb3grpr2  29673  upgr2wlk  29956  erclwwlkref  30311  erclwwlknref  30360  0spth  30417  0crct  30424  pjimai  32468  eulerpartlemt0  34703  bnj1101  35117  satfvsuclem2  35750  bj-snglc  37492  bj-epelb  37592  bj-opelidb1  37684  icorempo  37884  wl-cases2-dnf  38054  matunitlindf  38156  disjressuc2  38949  dflim5  43947  pm11.58  44991