Theorem pm2.21d 620

Description: A contradiction implies anything. Deduction from pm2.21 618. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
2		pm2.21 618	. 2 ⊢ (¬ 𝜓 → (𝜓 → 𝜒))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 616

This theorem is referenced by:  pm2.21dd  621  pm5.21  696  2falsed  703  mtord  784  prlem1  975  eq0rdv  3496  csbprc  3497  rzal  3549  poirr2  5063  nnsucuniel  6562  nnawordex  6596  swoord2  6631  difinfsnlem  7174  exmidomni  7217  elni2  7400  cauappcvgprlemdisj  7737  caucvgprlemdisj  7760  caucvgprprlemdisj  7788  caucvgsr  7888  lelttr  8134  nnsub  9048  nn0ge2m1nn  9328  elnnz  9355  elnn0z  9358  indstr  9686  indstr2  9702  xrltnsym  9887  xrlttr  9889  xrltso  9890  xrlelttr  9900  xltnegi  9929  xsubge0  9975  ixxdisj  9997  icodisj  10086  fzm1  10194  qbtwnxr  10366  frec2uzlt2d  10515  nn0ltexp2  10820  facdiv  10849  resqrexlemgt0  11204  climuni  11477  fsumcl2lem  11582  dvdsle  12028  prmdvdsexpr  12345  prmfac1  12347  sqrt2irr  12357  phibndlem  12411  dvdsprmpweqle  12533  isxmet2d  14670  lgsdir2lem2  15356  lgseisenlem2  15398  trilpolemres  15777