Theorem pm4.71d 560

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  pm4.71rd  561  rabeqcda  3441  difin2  4290  resopab2  6035  ordtri3  6399  onunel  6468  resoprab2  7529  psgnran  19424  efgcpbllemb  19664  cndis  23015  cnindis  23016  cnpdis  23017  blpnf  24123  dscopn  24302  itgcn  25594  limcnlp  25627  2sqreultlem  27186  2sqreunnltlem  27189  dfcgrg2  28381  nb3gr2nb  28908  uspgr2wlkeq  29170  upgrspthswlk  29262  wspthsnwspthsnon  29437  wpthswwlks2on  29482  1stpreima  32195  cntzsnid  32483  qusxpid  32749  qsfld  32886  ressply1mon1p  32931  fsumcvg4  33228  mbfmcnt  33565  satfv0  34647  topdifinffinlem  36531  phpreu  36775  ptrest  36790  rngosn3  37095  isidlc  37186  dih1  40460  prjsperref  41650  lzunuz  41808  nadd1suc  42444  naddsuc2  42445  fsovrfovd  43062  uneqsn  43078  itsclquadeu  47550  pm4.71da  47562  i0oii  47639  io1ii  47640