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  3408  difin2  4254  resopab2  5991  ordtri3  6347  onunel  6418  resoprab2  7472  naddsuc2  8626  psgnran  19413  efgcpbllemb  19653  cndis  23195  cnindis  23196  cnpdis  23197  blpnf  24302  dscopn  24478  itgcn  25763  limcnlp  25796  2sqreultlem  27375  2sqreunnltlem  27378  dfcgrg2  28827  nb3gr2nb  29348  uspgr2wlkeq  29610  upgrspthswlk  29702  wspthsnwspthsnon  29880  wpthswwlks2on  29925  1stpreima  32668  cntzsnid  33041  erler  33224  subsdrg  33256  qusxpid  33319  qsfld  33454  ressply1mon1p  33522  fsumcvg4  33936  mbfmcnt  34255  satfv0  35350  topdifinffinlem  37340  phpreu  37603  ptrest  37618  rngosn3  37923  isidlc  38014  dih1  41285  redvmptabs  42353  prjsperref  42599  lzunuz  42761  nadd1suc  43385  fsovrfovd  44002  uneqsn  44018  itsclquadeu  48782  pm4.71da  48794  i0oii  48924  io1ii  48925