Theorem pm4.71d 664

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

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

This theorem is referenced by:  difin2  3849  resopab2  5368  ordtri3  5676  fcnvres  5995  resoprab2  6655  psgnran  17758  efgcpbllemb  17991  cndis  20905  cnindis  20906  cnpdis  20907  blpnf  22012  dscopn  22188  itgcn  23415  limcnlp  23448  nb3gra2nb  25984  usg2wlkeq  26236  clwwlkn2  26303  1stpreima  28867  fsumcvg4  29324  mbfmcnt  29657  topdifinffinlem  32371  phpreu  32563  ptrest  32578  rngosn3  32893  isidlc  32984  dih1  35593  lzunuz  36349  fsovrfovd  37323  uneqsn  37341  nb3gr2nb  40612  uspgr2wlkeq  40854  upgrspths1wlk  40944  wspthsnwspthsnon  41122  wpthswwlks2on  41164