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  3455  difin2  4320  resopab2  6065  ordtri3  6431  onunel  6500  resoprab2  7569  naddsuc2  8757  psgnran  19557  efgcpbllemb  19797  cndis  23320  cnindis  23321  cnpdis  23322  blpnf  24428  dscopn  24607  itgcn  25900  limcnlp  25933  2sqreultlem  27509  2sqreunnltlem  27512  dfcgrg2  28889  nb3gr2nb  29419  uspgr2wlkeq  29682  upgrspthswlk  29774  wspthsnwspthsnon  29949  wpthswwlks2on  29994  1stpreima  32718  cntzsnid  33045  erler  33237  qusxpid  33356  qsfld  33491  ressply1mon1p  33558  fsumcvg4  33896  mbfmcnt  34233  satfv0  35326  topdifinffinlem  37313  phpreu  37564  ptrest  37579  rngosn3  37884  isidlc  37975  dih1  41243  prjsperref  42561  lzunuz  42724  nadd1suc  43354  fsovrfovd  43971  uneqsn  43987  itsclquadeu  48511  pm4.71da  48523  i0oii  48599  io1ii  48600