Theorem pm4.71d 570

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  pm4.71rd  571  pm4.71da  572  rabeqcda  3434  difin2  4262  resopab2  6036  ordtri3  6394  onunel  6465  resoprab2  7527  naddsuc2  8684  qusxpid  19247  psgnran  19581  efgcpbllemb  19821  cndis  23413  cnindis  23414  cnpdis  23415  blpnf  24519  dscopn  24695  itgcn  25969  limcnlp  26002  2sqreultlem  27573  2sqreunnltlem  27576  dfcgrg2  29131  nb3gr2nb  29671  uspgr2wlkeq  29932  upgrspthswlk  30024  wspthsnwspthsnon  30202  wpthswwlks2on  30250  1stpreima  32989  cntzsnid  33337  isunitc  33498  erler  33522  subsdrg  33558  qsfld  33721  ressply1mon1p  33799  fsumcvg4  34281  mbfmcnt  34599  satfv0  35745  topdifinffinlem  37876  phpreu  38138  ptrest  38153  rngosn3  38458  isidlc  38549  dih1  41945  redvmptabs  43004  prjsperref  43223  lzunuz  43384  nadd1suc  44004  fsovrfovd  44620  uneqsn  44636  itsclquadeu  49435  i0oii  49576  io1ii  49577