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  5121  nnsucuniel  6649  nnawordex  6683  swoord2  6718  difinfsnlem  7274  exmidomni  7317  elni2  7509  cauappcvgprlemdisj  7846  caucvgprlemdisj  7869  caucvgprprlemdisj  7897  caucvgsr  7997  lelttr  8243  nnsub  9157  nn0ge2m1nn  9437  elnnz  9464  elnn0z  9467  indstr  9796  indstr2  9812  xrltnsym  9997  xrlttr  9999  xrltso  10000  xrlelttr  10010  xltnegi  10039  xsubge0  10085  ixxdisj  10107  icodisj  10196  fzm1  10304  qbtwnxr  10485  frec2uzlt2d  10634  nn0ltexp2  10939  facdiv  10968  resqrexlemgt0  11539  climuni  11812  fsumcl2lem  11917  dvdsle  12363  prmdvdsexpr  12680  prmfac1  12682  sqrt2irr  12692  phibndlem  12746  dvdsprmpweqle  12868  isxmet2d  15030  lgsdir2lem2  15716  lgseisenlem2  15758  wlkv0  16090  trilpolemres  16440