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  3425  difin2  4250  resopab2  6036  ordtri3  6398  onunel  6469  resoprab2  7536  naddsuc2  8694  qusxpid  19314  psgnran  19648  efgcpbllemb  19888  cndis  23522  cnindis  23523  cnpdis  23524  blpnf  24629  dscopn  24805  itgcn  26079  limcnlp  26112  2sqreultlem  27691  2sqreunnltlem  27694  dfcgrg2  29295  nb3gr2nb  29852  uspgr2wlkeq  30113  upgrspthswlk  30211  wspthsnwspthsnon  30392  wpthswwlks2on  30440  1stpreima  33187  cntzsnid  33528  isunitc  33689  erler  33713  subsdrg  33747  qsfld  33908  ressply1mon1p  33986  fsumcvg4  34468  mbfmcnt  34787  satfv0  35945  topdifinffinlem  38109  phpreu  38366  ptrest  38376  rngosn3  38682  isidlc  38773  dih1  42167  redvmptabs  43243  prjsperref  43460  lzunuz  43621  nadd1suc  44241  fsovrfovd  44857  uneqsn  44873  itsclquadeu  49715  i0oii  49854  io1ii  49855