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  828  pm4.45  999  eu6lem  2570  2eu5  2653  rabeqcOLD  3692  dfid2  5584  imadmrn  6089  dff1o2  6853  f12dfv  7292  isof1oidb  7343  isof1oopb  7344  xpsnen  9093  dom0OLD  9141  dfac5lem2  10161  axgroth6  10865  eqreznegel  12973  xrnemnf  13156  xrnepnf  13157  dfrp2  13432  elioopnf  13479  elioomnf  13480  elicopnf  13481  elxrge0  13493  isprm2  16715  efgrelexlemb  19782  opsrtoslem1  22096  tgphaus  24140  cfilucfil3  25367  ioombl1lem4  25609  vitalilem1  25656  ellogdm  26695  nb3grpr2  29414  upgr2wlk  29700  erclwwlkref  30048  erclwwlknref  30097  0spth  30154  0crct  30161  pjimai  32204  eulerpartlemt0  34350  bnj1101  34776  satfvsuclem2  35344  bj-snglc  36951  bj-epelb  37051  bj-opelidb1  37135  icorempo  37333  wl-cases2-dnf  37492  matunitlindf  37604  disjressuc2  38369  dflim5  43318  pm11.58  44385