Theorem pm4.71d 561

Description: Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)

Hypothesis

Ref	Expression
pm4.71rd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
pm4.71d	⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Proof of Theorem pm4.71d

Step	Hyp	Ref	Expression
1		pm4.71rd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		pm4.71 557	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	sylib 218	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.71rd  562  rabeqcda  3412  difin2  4255  resopab2  6003  ordtri3  6361  onunel  6432  resoprab2  7487  naddsuc2  8639  psgnran  19456  efgcpbllemb  19696  cndis  23247  cnindis  23248  cnpdis  23249  blpnf  24353  dscopn  24529  itgcn  25814  limcnlp  25847  2sqreultlem  27426  2sqreunnltlem  27429  dfcgrg2  28947  nb3gr2nb  29469  uspgr2wlkeq  29731  upgrspthswlk  29823  wspthsnwspthsnon  30001  wpthswwlks2on  30049  1stpreima  32797  cntzsnid  33174  erler  33359  subsdrg  33392  qusxpid  33456  qsfld  33591  ressply1mon1p  33661  fsumcvg4  34128  mbfmcnt  34446  satfv0  35574  topdifinffinlem  37602  phpreu  37855  ptrest  37870  rngosn3  38175  isidlc  38266  dih1  41662  redvmptabs  42730  prjsperref  42964  lzunuz  43125  nadd1suc  43749  fsovrfovd  44365  uneqsn  44381  itsclquadeu  49137  pm4.71da  49149  i0oii  49279  io1ii  49280