Theorem pm4.71d 561

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  pm4.71rd  562  rabeqcda  3445  difin2  4307  resopab2  6056  ordtri3  6422  onunel  6491  resoprab2  7552  naddsuc2  8738  psgnran  19548  efgcpbllemb  19788  cndis  23315  cnindis  23316  cnpdis  23317  blpnf  24423  dscopn  24602  itgcn  25895  limcnlp  25928  2sqreultlem  27506  2sqreunnltlem  27509  dfcgrg2  28886  nb3gr2nb  29416  uspgr2wlkeq  29679  upgrspthswlk  29771  wspthsnwspthsnon  29946  wpthswwlks2on  29991  1stpreima  32722  cntzsnid  33055  erler  33252  qusxpid  33371  qsfld  33506  ressply1mon1p  33573  fsumcvg4  33911  mbfmcnt  34250  satfv0  35343  topdifinffinlem  37330  phpreu  37591  ptrest  37606  rngosn3  37911  isidlc  38002  dih1  41269  redvmptabs  42369  prjsperref  42593  lzunuz  42756  nadd1suc  43382  fsovrfovd  43999  uneqsn  44015  itsclquadeu  48627  pm4.71da  48639  i0oii  48716  io1ii  48717