Theorem pm2.21d 622

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

This theorem is referenced by:  pm2.21dd  623  pm5.21  700  2falsed  707  mtord  788  prlem1  979  eq0rdv  3536  csbprc  3537  rzal  3589  poirr2  5124  nnsucuniel  6654  nnawordex  6688  swoord2  6723  difinfsnlem  7282  exmidomni  7325  elni2  7517  cauappcvgprlemdisj  7854  caucvgprlemdisj  7877  caucvgprprlemdisj  7905  caucvgsr  8005  lelttr  8251  nnsub  9165  nn0ge2m1nn  9445  elnnz  9472  elnn0z  9475  indstr  9805  indstr2  9821  xrltnsym  10006  xrlttr  10008  xrltso  10009  xrlelttr  10019  xltnegi  10048  xsubge0  10094  ixxdisj  10116  icodisj  10205  fzm1  10313  qbtwnxr  10494  frec2uzlt2d  10643  nn0ltexp2  10948  facdiv  10977  resqrexlemgt0  11552  climuni  11825  fsumcl2lem  11930  dvdsle  12376  prmdvdsexpr  12693  prmfac1  12695  sqrt2irr  12705  phibndlem  12759  dvdsprmpweqle  12881  isxmet2d  15043  lgsdir2lem2  15729  lgseisenlem2  15771  wlkv0  16141  trilpolemres  16524