Theorem pm4.71d 562

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 558	. 2 ⊢ ((𝜓 → 𝜒) ↔ (𝜓 ↔ (𝜓 ∧ 𝜒)))
3	1, 2	sylib 217	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  pm4.71rd  563  rabeqcda  3443  difin2  4291  resopab2  6036  ordtri3  6400  onunel  6469  resoprab2  7526  psgnran  19382  efgcpbllemb  19622  cndis  22794  cnindis  22795  cnpdis  22796  blpnf  23902  dscopn  24081  itgcn  25361  limcnlp  25394  2sqreultlem  26947  2sqreunnltlem  26950  dfcgrg2  28111  nb3gr2nb  28638  uspgr2wlkeq  28900  upgrspthswlk  28992  wspthsnwspthsnon  29167  wpthswwlks2on  29212  1stpreima  31923  cntzsnid  32208  qusxpid  32470  qsfld  32607  ressply1mon1p  32652  fsumcvg4  32925  mbfmcnt  33262  satfv0  34344  topdifinffinlem  36223  phpreu  36467  ptrest  36482  rngosn3  36787  isidlc  36878  dih1  40152  prjsperref  41349  lzunuz  41496  nadd1suc  42132  naddsuc2  42133  fsovrfovd  42750  uneqsn  42766  itsclquadeu  47453  pm4.71da  47465  i0oii  47542  io1ii  47543