Theorem pm4.71d 571

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  pm4.71rd  572  pm4.71da  573  rabeqcda  3423  difin2  4245  resopab2  6030  ordtri3  6402  onunel  6473  resoprab2  7543  naddsuc2  8718  qusxpid  19404  psgnran  19738  efgcpbllemb  19978  cndis  23618  cnindis  23619  cnpdis  23620  blpnf  24725  dscopn  24901  itgcn  26174  limcnlp  26207  2sqreultlem  27783  2sqreunnltlem  27786  dfcgrg2  29417  nb3gr2nb  29974  uspgr2wlkeq  30235  upgrspthswlk  30333  wspthsnwspthsnon  30514  wpthswwlks2on  30562  1stpreima  33351  cntzsnid  33691  isunitc  33852  erler  33876  subsdrg  33910  qsfld  34072  ressply1mon1p  34150  fsumcvg4  34632  mbfmcnt  34950  satfv0  36213  topdifinffinlem  38379  phpreu  38636  ptrest  38646  rngosn3  38967  isidlc  39058  dih1  42452  redvmptabs  43520  prjsperref  43743  lzunuz  43888  nadd1suc  44503  fsovrfovd  45118  uneqsn  45134  itsclquadeu  49997  i0oii  50142  io1ii  50143