Theorem pm4.71d 564

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  pm4.71rd  565  difin2  4265  resopab2  5903  ordtri3  6226  resoprab2  7270  psgnran  18642  efgcpbllemb  18880  cndis  21898  cnindis  21899  cnpdis  21900  blpnf  23006  dscopn  23182  itgcn  24442  limcnlp  24475  2sqreultlem  26022  2sqreunnltlem  26025  dfcgrg2  26648  nb3gr2nb  27165  uspgr2wlkeq  27426  upgrspthswlk  27518  wspthsnwspthsnon  27694  wpthswwlks2on  27739  1stpreima  30441  cntzsnid  30696  qusxpid  30928  fsumcvg4  31193  mbfmcnt  31526  satfv0  32605  topdifinffinlem  34627  phpreu  34875  ptrest  34890  rngosn3  35201  isidlc  35292  dih1  38421  rabeqcda  39104  prjsperref  39254  lzunuz  39363  fsovrfovd  40353  uneqsn  40371  itsclquadeu  44763