Theorem pm2.21d 624

Description: A contradiction implies anything. Deduction from pm2.21 622. (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 622	. 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 620

This theorem is referenced by:  pm2.21dd  625  pm5.21  703  2falsed  710  mtord  791  prlem1  982  eq0rdv  3552  csbprc  3553  rzal  3606  poirr2  5154  nnsucuniel  6727  nnawordex  6761  swoord2  6796  difinfsnlem  7389  exmidomni  7432  elni2  7625  cauappcvgprlemdisj  7962  caucvgprlemdisj  7985  caucvgprprlemdisj  8013  caucvgsr  8113  lelttr  8358  nnsub  9272  nn0ge2m1nn  9556  elnnz  9583  elnn0z  9586  indstr  9921  indstr2  9937  xrltnsym  10122  xrlttr  10124  xrltso  10125  xrlelttr  10135  xltnegi  10164  xsubge0  10210  ixxdisj  10232  icodisj  10321  fzm1  10430  qbtwnxr  10613  frec2uzlt2d  10762  nn0ltexp2  11067  facdiv  11096  resqrexlemgt0  11698  climuni  11971  fsumcl2lem  12077  dvdsle  12523  prmdvdsexpr  12840  prmfac1  12842  sqrt2irr  12852  phibndlem  12906  dvdsprmpweqle  13028  isxmet2d  15200  lgsdir2lem2  15889  lgseisenlem2  15931  wlkv0  16351  trilpolemres  16813