Theorem pm4.71d 562

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

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

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 397

This theorem is referenced by:  pm4.71rd  563  rabeqcda  3429  difin2  4225  resopab2  5944  ordtri3  6302  resoprab2  7393  psgnran  19123  efgcpbllemb  19361  cndis  22442  cnindis  22443  cnpdis  22444  blpnf  23550  dscopn  23729  itgcn  25009  limcnlp  25042  2sqreultlem  26595  2sqreunnltlem  26598  dfcgrg2  27224  nb3gr2nb  27751  uspgr2wlkeq  28013  upgrspthswlk  28106  wspthsnwspthsnon  28281  wpthswwlks2on  28326  1stpreima  31039  cntzsnid  31321  qusxpid  31559  fsumcvg4  31900  mbfmcnt  32235  satfv0  33320  onunel  33689  topdifinffinlem  35518  phpreu  35761  ptrest  35776  rngosn3  36082  isidlc  36173  dih1  39300  prjsperref  40445  lzunuz  40590  fsovrfovd  41617  uneqsn  41633  itsclquadeu  46123  pm4.71da  46135  i0oii  46213  io1ii  46214