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  3417  difin2  4264  resopab2  6007  ordtri3  6368  onunel  6439  resoprab2  7508  naddsuc2  8665  psgnran  19445  efgcpbllemb  19685  cndis  23178  cnindis  23179  cnpdis  23180  blpnf  24285  dscopn  24461  itgcn  25746  limcnlp  25779  2sqreultlem  27358  2sqreunnltlem  27361  dfcgrg2  28790  nb3gr2nb  29311  uspgr2wlkeq  29574  upgrspthswlk  29668  wspthsnwspthsnon  29846  wpthswwlks2on  29891  1stpreima  32630  cntzsnid  33009  erler  33216  subsdrg  33248  qusxpid  33334  qsfld  33469  ressply1mon1p  33537  fsumcvg4  33940  mbfmcnt  34259  satfv0  35345  topdifinffinlem  37335  phpreu  37598  ptrest  37613  rngosn3  37918  isidlc  38009  dih1  41280  redvmptabs  42348  prjsperref  42594  lzunuz  42756  nadd1suc  43381  fsovrfovd  43998  uneqsn  44014  itsclquadeu  48763  pm4.71da  48775  i0oii  48905  io1ii  48906