Theorem pm4.71d 553

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  difin2  4091  resopab2  5653  ordtri3  5972  fcnvres  6293  resoprab2  6983  psgnran  18132  efgcpbllemb  18365  cndis  21306  cnindis  21307  cnpdis  21308  blpnf  22412  dscopn  22588  itgcn  23822  limcnlp  23855  nb3gr2nb  26501  uspgr2wlkeq  26769  upgrspthswlk  26861  wspthsnwspthsnon  27053  wspthsnwspthsnonOLD  27055  wpthswwlks2on  27101  wpthswwlks2onOLD  27102  1stpreima  29810  fsumcvg4  30320  mbfmcnt  30654  topdifinffinlem  33509  phpreu  33704  ptrest  33719  rngosn3  34032  isidlc  34123  dih1  37064  lzunuz  37830  fsovrfovd  38800  uneqsn  38818