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  3407  difin2  4250  resopab2  5992  ordtri3  6350  onunel  6421  resoprab2  7474  naddsuc2  8625  psgnran  19435  efgcpbllemb  19675  cndis  23226  cnindis  23227  cnpdis  23228  blpnf  24332  dscopn  24508  itgcn  25793  limcnlp  25826  2sqreultlem  27405  2sqreunnltlem  27408  dfcgrg2  28861  nb3gr2nb  29383  uspgr2wlkeq  29645  upgrspthswlk  29737  wspthsnwspthsnon  29915  wpthswwlks2on  29963  1stpreima  32712  cntzsnid  33090  erler  33275  subsdrg  33308  qusxpid  33372  qsfld  33507  ressply1mon1p  33577  fsumcvg4  34035  mbfmcnt  34353  satfv0  35474  topdifinffinlem  37464  phpreu  37717  ptrest  37732  rngosn3  38037  isidlc  38128  dih1  41458  redvmptabs  42530  prjsperref  42764  lzunuz  42925  nadd1suc  43549  fsovrfovd  44166  uneqsn  44182  itsclquadeu  48939  pm4.71da  48951  i0oii  49081  io1ii  49082