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 217	1 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  pm4.71rd  562  rabeqcda  3419  difin2  4222  resopab2  5933  ordtri3  6287  resoprab2  7371  psgnran  19038  efgcpbllemb  19276  cndis  22350  cnindis  22351  cnpdis  22352  blpnf  23458  dscopn  23635  itgcn  24914  limcnlp  24947  2sqreultlem  26500  2sqreunnltlem  26503  dfcgrg2  27128  nb3gr2nb  27654  uspgr2wlkeq  27915  upgrspthswlk  28007  wspthsnwspthsnon  28182  wpthswwlks2on  28227  1stpreima  30941  cntzsnid  31223  qusxpid  31461  fsumcvg4  31802  mbfmcnt  32135  satfv0  33220  onunel  33592  topdifinffinlem  35445  phpreu  35688  ptrest  35703  rngosn3  36009  isidlc  36100  dih1  39227  prjsperref  40366  lzunuz  40506  fsovrfovd  41506  uneqsn  41522  itsclquadeu  46011  pm4.71da  46023  i0oii  46101  io1ii  46102