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  697  2falsed  704  mtord  785  prlem1  976  eq0rdv  3506  csbprc  3507  rzal  3559  poirr2  5080  nnsucuniel  6588  nnawordex  6622  swoord2  6657  difinfsnlem  7208  exmidomni  7251  elni2  7434  cauappcvgprlemdisj  7771  caucvgprlemdisj  7794  caucvgprprlemdisj  7822  caucvgsr  7922  lelttr  8168  nnsub  9082  nn0ge2m1nn  9362  elnnz  9389  elnn0z  9392  indstr  9721  indstr2  9737  xrltnsym  9922  xrlttr  9924  xrltso  9925  xrlelttr  9935  xltnegi  9964  xsubge0  10010  ixxdisj  10032  icodisj  10121  fzm1  10229  qbtwnxr  10407  frec2uzlt2d  10556  nn0ltexp2  10861  facdiv  10890  resqrexlemgt0  11375  climuni  11648  fsumcl2lem  11753  dvdsle  12199  prmdvdsexpr  12516  prmfac1  12518  sqrt2irr  12528  phibndlem  12582  dvdsprmpweqle  12704  isxmet2d  14864  lgsdir2lem2  15550  lgseisenlem2  15592  trilpolemres  16055