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 219	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  pm4.71rd  563  difin2  4192  resopab2  5792  ordtri3  6109  resoprab2  7134  psgnran  18378  efgcpbllemb  18612  cndis  21587  cnindis  21588  cnpdis  21589  blpnf  22694  dscopn  22870  itgcn  24130  limcnlp  24163  2sqreultlem  25709  2sqreunnltlem  25712  dfcgrg2  26336  nb3gr2nb  26853  uspgr2wlkeq  27114  upgrspthswlk  27205  wspthsnwspthsnon  27381  wpthswwlks2on  27426  1stpreima  30126  cntzsnid  30503  fsumcvg4  30806  mbfmcnt  31139  satfv0  32215  topdifinffinlem  34180  phpreu  34428  ptrest  34443  rngosn3  34755  isidlc  34846  dih1  37974  rabeqcda  38657  prjsperref  38774  lzunuz  38871  fsovrfovd  39861  uneqsn  39879  itsclquadeu  44267