Theorem pm4.71d 669

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ 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 197  df-an 385

This theorem is referenced by:  difin2  4033  resopab2  5606  ordtri3  5920  fcnvres  6243  resoprab2  6923  psgnran  18155  efgcpbllemb  18388  cndis  21317  cnindis  21318  cnpdis  21319  blpnf  22423  dscopn  22599  itgcn  23828  limcnlp  23861  nb3gr2nb  26505  uspgr2wlkeq  26773  upgrspthswlk  26865  wspthsnwspthsnon  27055  wspthsnwspthsnonOLD  27057  wpthswwlks2on  27103  wpthswwlks2onOLD  27104  1stpreima  29814  fsumcvg4  30326  mbfmcnt  30660  topdifinffinlem  33524  phpreu  33724  ptrest  33739  rngosn3  34054  isidlc  34145  dih1  37095  lzunuz  37851  fsovrfovd  38823  uneqsn  38841