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  3400  difin2  4241  resopab2  6001  ordtri3  6359  onunel  6430  resoprab2  7486  naddsuc2  8637  psgnran  19490  efgcpbllemb  19730  cndis  23256  cnindis  23257  cnpdis  23258  blpnf  24362  dscopn  24538  itgcn  25812  limcnlp  25845  2sqreultlem  27410  2sqreunnltlem  27413  dfcgrg2  28931  nb3gr2nb  29453  uspgr2wlkeq  29714  upgrspthswlk  29806  wspthsnwspthsnon  29984  wpthswwlks2on  30032  1stpreima  32780  cntzsnid  33141  erler  33326  subsdrg  33359  qusxpid  33423  qsfld  33558  ressply1mon1p  33628  fsumcvg4  34094  mbfmcnt  34412  satfv0  35540  topdifinffinlem  37663  phpreu  37925  ptrest  37940  rngosn3  38245  isidlc  38336  dih1  41732  redvmptabs  42792  prjsperref  43039  lzunuz  43200  nadd1suc  43820  fsovrfovd  44436  uneqsn  44452  itsclquadeu  49253  pm4.71da  49265  i0oii  49395  io1ii  49396