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  3448  difin2  4301  resopab2  6054  ordtri3  6420  onunel  6489  resoprab2  7552  naddsuc2  8739  psgnran  19533  efgcpbllemb  19773  cndis  23299  cnindis  23300  cnpdis  23301  blpnf  24407  dscopn  24586  itgcn  25880  limcnlp  25913  2sqreultlem  27491  2sqreunnltlem  27494  dfcgrg2  28871  nb3gr2nb  29401  uspgr2wlkeq  29664  upgrspthswlk  29758  wspthsnwspthsnon  29936  wpthswwlks2on  29981  1stpreima  32716  cntzsnid  33072  erler  33269  qusxpid  33391  qsfld  33526  ressply1mon1p  33593  fsumcvg4  33949  mbfmcnt  34270  satfv0  35363  topdifinffinlem  37348  phpreu  37611  ptrest  37626  rngosn3  37931  isidlc  38022  dih1  41288  redvmptabs  42390  prjsperref  42616  lzunuz  42779  nadd1suc  43405  fsovrfovd  44022  uneqsn  44038  itsclquadeu  48698  pm4.71da  48710  i0oii  48817  io1ii  48818