Theorem pm4.71i 550

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 383

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 198  df-an 384

This theorem is referenced by:  pm4.24  554  anabs1  642  pm4.45  1009  2eu5  2709  rabeqc  3519  imadmrn  5627  dff1o2  6298  f12dfv  6691  isof1oidb  6736  isof1oopb  6737  xpsnen  8221  dom0  8265  dfac5lem2  9168  pwfseqlem4  9707  axgroth6  9873  eqreznegel  11999  xrnemnf  12173  xrnepnf  12174  elioopnf  12492  elioomnf  12493  elicopnf  12494  elxrge0  12507  isprm2  15623  efgrelexlemb  18390  opsrtoslem1  19719  tgphaus  22160  cfilucfil3  23356  ioombl1lem4  23569  vitalilem1  23616  ellogdm  24627  nb3grpr2  26529  upgr2wlk  26820  erclwwlkref  27191  erclwwlknref  27248  0spth  27327  0crct  27334  pjimai  29392  dfrp2  29889  eulerpartlemt0  30788  bnj1101  31210  bj-snglc  33305  icorempt2  33553  wl-cases2-dnf  33649  matunitlindf  33757  pm11.58  39130