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  3432  difin2  4281  resopab2  6028  ordtri3  6393  onunel  6464  resoprab2  7531  naddsuc2  8718  psgnran  19501  efgcpbllemb  19741  cndis  23234  cnindis  23235  cnpdis  23236  blpnf  24341  dscopn  24517  itgcn  25803  limcnlp  25836  2sqreultlem  27415  2sqreunnltlem  27418  dfcgrg2  28847  nb3gr2nb  29368  uspgr2wlkeq  29631  upgrspthswlk  29725  wspthsnwspthsnon  29903  wpthswwlks2on  29948  1stpreima  32689  cntzsnid  33068  erler  33265  subsdrg  33297  qusxpid  33383  qsfld  33518  ressply1mon1p  33586  fsumcvg4  33986  mbfmcnt  34305  satfv0  35385  topdifinffinlem  37370  phpreu  37633  ptrest  37648  rngosn3  37953  isidlc  38044  dih1  41310  redvmptabs  42370  prjsperref  42596  lzunuz  42758  nadd1suc  43383  fsovrfovd  44000  uneqsn  44016  itsclquadeu  48724  pm4.71da  48736  i0oii  48861  io1ii  48862