Theorem pm4.71d 551

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382

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 383

This theorem is referenced by:  difin2  4038  resopab2  5587  ordtri3  5900  fcnvres  6220  resoprab2  6904  psgnran  18138  efgcpbllemb  18371  cndis  21312  cnindis  21313  cnpdis  21314  blpnf  22418  dscopn  22594  itgcn  23825  limcnlp  23858  nb3gr2nb  26505  uspgr2wlkeq  26773  upgrspthswlk  26865  wspthsnwspthsnon  27057  wspthsnwspthsnonOLD  27059  wpthswwlks2on  27105  wpthswwlks2onOLD  27106  1stpreima  29820  fsumcvg4  30332  mbfmcnt  30666  topdifinffinlem  33528  phpreu  33722  ptrest  33737  rngosn3  34051  isidlc  34142  dih1  37093  lzunuz  37854  fsovrfovd  38826  uneqsn  38844