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  3414  difin2  4260  resopab2  5996  ordtri3  6356  onunel  6427  resoprab2  7488  naddsuc2  8642  psgnran  19421  efgcpbllemb  19661  cndis  23154  cnindis  23155  cnpdis  23156  blpnf  24261  dscopn  24437  itgcn  25722  limcnlp  25755  2sqreultlem  27334  2sqreunnltlem  27337  dfcgrg2  28766  nb3gr2nb  29287  uspgr2wlkeq  29549  upgrspthswlk  29641  wspthsnwspthsnon  29819  wpthswwlks2on  29864  1stpreima  32603  cntzsnid  32982  erler  33189  subsdrg  33221  qusxpid  33307  qsfld  33442  ressply1mon1p  33510  fsumcvg4  33913  mbfmcnt  34232  satfv0  35318  topdifinffinlem  37308  phpreu  37571  ptrest  37586  rngosn3  37891  isidlc  37982  dih1  41253  redvmptabs  42321  prjsperref  42567  lzunuz  42729  nadd1suc  43354  fsovrfovd  43971  uneqsn  43987  itsclquadeu  48739  pm4.71da  48751  i0oii  48881  io1ii  48882