Theorem pm4.71d 563

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

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

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 398

This theorem is referenced by:  pm4.71rd  564  rabeqcda  3444  difin2  4289  resopab2  6033  ordtri3  6396  onunel  6465  resoprab2  7521  psgnran  19375  efgcpbllemb  19615  cndis  22776  cnindis  22777  cnpdis  22778  blpnf  23884  dscopn  24063  itgcn  25343  limcnlp  25376  2sqreultlem  26929  2sqreunnltlem  26932  dfcgrg2  28093  nb3gr2nb  28620  uspgr2wlkeq  28882  upgrspthswlk  28974  wspthsnwspthsnon  29149  wpthswwlks2on  29194  1stpreima  31905  cntzsnid  32190  qusxpid  32443  qsfld  32564  ressply1mon1p  32603  fsumcvg4  32867  mbfmcnt  33204  satfv0  34286  topdifinffinlem  36165  phpreu  36409  ptrest  36424  rngosn3  36729  isidlc  36820  dih1  40094  prjsperref  41291  lzunuz  41438  nadd1suc  42074  naddsuc2  42075  fsovrfovd  42692  uneqsn  42708  itsclquadeu  47364  pm4.71da  47376  i0oii  47453  io1ii  47454