Theorem pm4.71d 566

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  pm4.71rd  567  rabeqcda  3402  difin2  4229  resopab2  5988  ordtri3  6346  onunel  6417  resoprab2  7475  naddsuc2  8627  psgnran  19481  efgcpbllemb  19721  cndis  23274  cnindis  23275  cnpdis  23276  blpnf  24380  dscopn  24556  itgcn  25830  limcnlp  25863  2sqreultlem  27428  2sqreunnltlem  27431  dfcgrg2  28949  nb3gr2nb  29471  uspgr2wlkeq  29732  upgrspthswlk  29824  wspthsnwspthsnon  30002  wpthswwlks2on  30050  1stpreima  32799  cntzsnid  33161  erler  33346  subsdrg  33382  qusxpid  33446  qsfld  33581  ressply1mon1p  33651  fsumcvg4  34134  mbfmcnt  34452  satfv0  35586  topdifinffinlem  37709  phpreu  37971  ptrest  37986  rngosn3  38291  isidlc  38382  dih1  41778  redvmptabs  42837  prjsperref  43056  lzunuz  43217  nadd1suc  43837  fsovrfovd  44453  uneqsn  44469  itsclquadeu  49268  pm4.71da  49280  i0oii  49410  io1ii  49411