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  2571  2eu5  2654  dfid2  5519  imadmrn  6027  dff1o2  6777  f12dfv  7217  isof1oidb  7268  isof1oopb  7269  xpsnen  8987  dfac5lem2  10032  axgroth6  10737  eqreznegel  12845  xrnemnf  13029  xrnepnf  13030  dfrp2  13308  elioopnf  13357  elioomnf  13358  elicopnf  13359  elxrge0  13371  isprm2  16607  efgrelexlemb  19677  opsrtoslem1  22008  tgphaus  24059  cfilucfil3  25274  ioombl1lem4  25516  vitalilem1  25563  ellogdm  26602  nb3grpr2  29405  upgr2wlk  29689  erclwwlkref  30044  erclwwlknref  30093  0spth  30150  0crct  30157  pjimai  32200  eulerpartlemt0  34475  bnj1101  34889  satfvsuclem2  35503  bj-snglc  37113  bj-epelb  37213  bj-opelidb1  37297  icorempo  37495  wl-cases2-dnf  37656  matunitlindf  37758  disjressuc2  38535  dflim5  43513  pm11.58  44573