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  3429  difin2  4254  resopab2  6040  ordtri3  6401  onunel  6472  resoprab2  7535  naddsuc2  8690  qusxpid  19275  psgnran  19609  efgcpbllemb  19849  cndis  23478  cnindis  23479  cnpdis  23480  blpnf  24585  dscopn  24761  itgcn  26035  limcnlp  26068  2sqreultlem  27642  2sqreunnltlem  27645  dfcgrg2  29211  nb3gr2nb  29768  uspgr2wlkeq  30029  upgrspthswlk  30127  wspthsnwspthsnon  30308  wpthswwlks2on  30356  1stpreima  33099  cntzsnid  33440  isunitc  33601  erler  33625  subsdrg  33659  qsfld  33820  ressply1mon1p  33898  fsumcvg4  34380  mbfmcnt  34699  satfv0  35863  topdifinffinlem  38026  phpreu  38288  ptrest  38303  rngosn3  38608  isidlc  38699  dih1  42093  redvmptabs  43154  prjsperref  43371  lzunuz  43532  nadd1suc  44152  fsovrfovd  44768  uneqsn  44784  itsclquadeu  49590  i0oii  49731  io1ii  49732