Theorem pm2.21d 121

Description: A contradiction implies anything. Deduction associated with pm2.21 123. (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	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	1 ⊢ (𝜑 → (𝜓 → 𝜒))

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm2.21ddALT  122  pm2.21  123  pm2.521g  174  prlem1  1054  sbc2or  3762  eq0rdvALT  4371  rzalALT  4473  reusv2lem2  5354  po2ne  5562  poirr2  6097  sofld  6160  dfwe2  7750  tfindsg  7837  findsg  7873  omopth2  8548  swoord2  8704  unxpdomlem3  9199  preleqg  9568  suc11reg  9572  wemapwe  9650  r111  9728  r1pwss  9737  cflim2  10216  axunndlem1  10548  axunnd  10549  axpowndlem3  10552  axpownd  10554  axregndlem1  10555  axregndlem2  10556  axinfndlem1  10558  axinfnd  10559  axacndlem1  10560  axacndlem2  10561  axacndlem3  10562  axacndlem4  10563  axacndlem5  10564  axacnd  10565  fpwwe2lem12  10595  gchpwdom  10623  winalim2  10649  ltapr  10998  prodgt0  12029  squeeze0  12086  nnsub  12230  nn0sub  12492  elnnz  12539  nn0lt10b  12596  indstr2  12886  uzsupss  12899  nn01to3  12900  xrltnsym  13097  xrlttr  13100  qbtwnxr  13160  xltnegi  13176  xmullem  13224  xlemul1a  13248  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  xrsup0  13283  xrinf0  13299  reltxrnmnf  13303  ixxdisj  13321  icodisj  13437  fzm1  13568  addmodlteq  13911  facdiv  14252  hasheqf1oi  14316  relexpfld  15015  relexpuzrel  15018  reusq0  15431  climuni  15518  rlimno1  15620  sqrt2irr  16217  nn0rppwr  16531  prmdvdsexpr  16687  prmfac1  16690  dvdsprmpweqle  16857  ramlb  16990  ram0  16993  prmgaplem6  17027  prmlem1  17078  prmlem2  17090  pospo  18304  efgredlemc  19675  efgred  19678  ablsimpnosubgd  20036  sdrgacs  20710  prmirred  21384  psrvscafval  21857  fvmptnn04ifa  22737  fvmptnn04ifb  22738  fvmptnn04ifc  22739  fvmptnn04ifd  22740  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  0top  22870  pnfnei  23107  mnfnei  23108  cmpfi  23295  1stccnp  23349  filconn  23770  ivthlem2  25353  ivthlem3  25354  ovolicc2lem3  25420  itg1addlem4  25600  itg2seq  25643  dvcnvlem  25880  lhop2  25920  bpos1  27194  lgsdir2lem2  27237  lgsqrlem2  27258  lgseisenlem2  27287  2sqnn  27350  pntlem3  27520  ostth3  27549  nosupbnd1lem5  27624  noinfbnd1lem5  27639  noetasuplem4  27648  noetainflem4  27652  elnnzs  28289  expsne0  28321  tgcgr4  28458  axlowdimlem15  28883  nbusgrvtxm1  29306  wlkv0  29579  1to2vfriswmgr  30208  n4cyclfrgr  30220  frgrnbnb  30222  frgrregord013  30324  snsssng  32443  ifeqeqx  32471  rprmdvdsprod  33505  fldext2chn  33718  f1resrcmplf1dlem  35076  erdszelem4  35181  erdszelem8  35185  antnestlaw3lem  35677  finminlem  36306  nn0prpwlem  36310  nn0prpw  36311  ordcmp  36435  iooelexlt  37350  relowlssretop  37351  smprngopr  38046  disjlem14  38790  prtlem14  38867  atltcvr  39429  dihord6apre  41250  dihord6b  41254  jm2.23  42985  onexlimgt  43232  ordnexbtwnsuc  43256  onov0suclim  43263  relexpmulg  43699  rzalf  45011  or2expropbi  47035  icceuelpart  47437  iccpartnel  47439  poprelb  47525  goldbachthlem2  47547  fmtnoprmfac1  47566  fmtnoprmfac2  47568  fmtno4prmfac  47573  fmtno4prmfac193  47574  2pwp1prm  47590  lighneallem4  47611  requad1  47623  requad2  47624  evenprm2  47715  odd2prm2  47719  stgoldbwt  47777  sbgoldbwt  47778  sbgoldbalt  47782  usgrexmpl12ngric  48029  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem5  48113  ztprmneprm  48335  functermc  49497