Theorem pm4.71d 569

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  pm4.71rd  570  rabeqcda  3424  difin2  4251  resopab2  6021  ordtri3  6377  onunel  6448  resoprab2  7510  naddsuc2  8666  psgnran  19546  efgcpbllemb  19786  cndis  23339  cnindis  23340  cnpdis  23341  blpnf  24445  dscopn  24621  itgcn  25895  limcnlp  25928  2sqreultlem  27499  2sqreunnltlem  27502  dfcgrg2  29020  nb3gr2nb  29542  uspgr2wlkeq  29803  upgrspthswlk  29895  wspthsnwspthsnon  30073  wpthswwlks2on  30121  1stpreima  32870  cntzsnid  33221  isunitc  33383  erler  33407  subsdrg  33446  qusxpid  33510  qsfld  33647  ressply1mon1p  33725  fsumcvg4  34208  mbfmcnt  34526  satfv0  35669  topdifinffinlem  37802  phpreu  38064  ptrest  38079  rngosn3  38384  isidlc  38475  dih1  41871  redvmptabs  42930  prjsperref  43149  lzunuz  43310  nadd1suc  43930  fsovrfovd  44546  uneqsn  44562  itsclquadeu  49360  pm4.71da  49372  i0oii  49502  io1ii  49503