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  3557  csbprc  3558  rzal  3611  ifeqeqxdc  3673  poirr2  5160  nnsucuniel  6741  nnawordex  6775  swoord2  6810  difinfsnlem  7403  exmidomni  7446  elni2  7645  cauappcvgprlemdisj  7982  caucvgprlemdisj  8005  caucvgprprlemdisj  8033  caucvgsr  8133  lelttr  8378  nnsub  9296  nn0ge2m1nn  9580  elnnz  9607  elnn0z  9610  indstr  9946  indstr2  9962  xrltnsym  10148  xrlttr  10150  xrltso  10151  xrlelttr  10161  xltnegi  10190  xsubge0  10236  ixxdisj  10258  icodisj  10347  fzm1  10459  qbtwnxr  10644  frec2uzlt2d  10793  nn0ltexp2  11099  facdiv  11128  resqrexlemgt0  11733  climuni  12006  fsumcl2lem  12112  dvdsle  12558  prmdvdsexpr  12875  prmfac1  12877  sqrt2irr  12887  phibndlem  12941  dvdsprmpweqle  13063  isxmet2d  15342  lgsdir2lem2  16031  lgseisenlem2  16073  wlkv0  16493  trilpolemres  16965