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  3410  difin2  4253  resopab2  5995  ordtri3  6353  onunel  6424  resoprab2  7477  naddsuc2  8629  psgnran  19444  efgcpbllemb  19684  cndis  23235  cnindis  23236  cnpdis  23237  blpnf  24341  dscopn  24517  itgcn  25802  limcnlp  25835  2sqreultlem  27414  2sqreunnltlem  27417  dfcgrg2  28935  nb3gr2nb  29457  uspgr2wlkeq  29719  upgrspthswlk  29811  wspthsnwspthsnon  29989  wpthswwlks2on  30037  1stpreima  32786  cntzsnid  33162  erler  33347  subsdrg  33380  qusxpid  33444  qsfld  33579  ressply1mon1p  33649  fsumcvg4  34107  mbfmcnt  34425  satfv0  35552  topdifinffinlem  37552  phpreu  37805  ptrest  37820  rngosn3  38125  isidlc  38216  dih1  41546  redvmptabs  42615  prjsperref  42849  lzunuz  43010  nadd1suc  43634  fsovrfovd  44250  uneqsn  44266  itsclquadeu  49023  pm4.71da  49035  i0oii  49165  io1ii  49166