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  1063  sbc2or  3748  eq0rdvALT  4356  rzalALT  4443  reusv2lem2  5350  iunopeqop  5484  po2ne  5564  poirr2  6101  sofld  6162  dfwe2  7746  tfindsg  7830  findsg  7867  omopth2  8541  swoord2  8700  unxpdomlem3  9191  preleqg  9560  suc11reg  9564  wemapwe  9642  r111  9723  r1pwss  9732  cflim2  10210  axunndlem1  10543  axunnd  10544  axpowndlem3  10547  axpownd  10549  axregndlem1  10550  axregndlem2  10551  axinfndlem1  10553  axinfnd  10554  axacndlem1  10555  axacndlem2  10556  axacndlem3  10557  axacndlem4  10558  axacndlem5  10559  axacnd  10560  fpwwe2lem12  10590  gchpwdom  10618  winalim2  10644  ltapr  10993  prodgt0  12028  squeeze0  12085  nnsub  12247  nn0sub  12521  elnnz  12568  nn0lt10b  12625  indstr2  12918  uzsupss  12931  nn01to3  12932  xrltnsym  13129  xrlttr  13132  qbtwnxr  13193  xltnegi  13209  xmullem  13257  xlemul1a  13281  xrsupsslem  13300  xrinfmsslem  13301  xrub  13305  xrsup0  13316  xrinf0  13332  reltxrnmnf  13336  ixxdisj  13354  icodisj  13470  fzm1  13602  addmodlteq  13949  facdiv  14290  hasheqf1oi  14354  relexpfld  15052  relexpuzrel  15055  reusq0  15468  climuni  15555  rlimno1  15657  sqrt2irr  16257  nn0rppwr  16571  prmdvdsexpr  16728  prmfac1  16731  dvdsprmpweqle  16898  ramlb  17031  ram0  17034  prmgaplem6  17068  prmlem1  17119  prmlem2  17132  pospo  18351  efgredlemc  19761  efgred  19764  ablsimpnosubgd  20122  sdrgacs  20823  prmirred  21499  psrvscafval  21973  fvmptnn04ifa  22883  fvmptnn04ifb  22884  fvmptnn04ifc  22885  fvmptnn04ifd  22886  chfacfscmulgsum  22893  chfacfpmmulgsum  22897  0top  23016  pnfnei  23253  mnfnei  23254  cmpfi  23441  1stccnp  23495  filconn  23916  ivthlem2  25487  ivthlem3  25488  ovolicc2lem3  25554  itg1addlem4  25734  itg2seq  25777  dvcnvlem  26011  lhop2  26050  bpos1  27317  lgsdir2lem2  27360  lgsqrlem2  27381  lgseisenlem2  27410  2sqnn  27473  pntlem3  27643  ostth3  27672  nosupbnd1lem5  27746  noinfbnd1lem5  27761  noetasuplem4  27770  noetainflem4  27774  elnnzs  28464  expsne0  28499  tgcgr4  28670  axlowdimlem15  29096  nbusgrvtxm1  29519  wlkv0  29789  1to2vfriswmgr  30420  n4cyclfrgr  30432  frgrnbnb  30434  frgrregord013  30536  snsssng  32655  ifeqeqx  32683  rprmdvdsprod  33684  fldext2chn  33979  f1resrcmplf1dlem  35337  erdszelem4  35492  erdszelem8  35496  antnestlaw3lem  35988  finminlem  36626  nn0prpwlem  36630  nn0prpw  36631  ordcmp  36755  axtcond  36786  mh-setindnd  36845  iooelexlt  37804  relowlssretop  37805  smprngopr  38499  disjlem14  39348  prtlem14  39446  atltcvr  40007  dihord6apre  41828  dihord6b  41832  jm2.23  43521  onexlimgt  43768  ordnexbtwnsuc  43792  onov0suclim  43799  relexpmulg  44234  rzalf  45545  or2expropbi  47576  nnmul2  47872  icceuelpart  47990  iccpartnel  47992  poprelb  48078  goldbachthlem2  48103  fmtnoprmfac1  48122  fmtnoprmfac2  48124  fmtno4prmfac  48129  fmtno4prmfac193  48130  2pwp1prm  48146  lighneallem4  48167  requad1  48192  requad2  48193  evenprm2  48284  odd2prm2  48288  stgoldbwt  48346  sbgoldbwt  48347  sbgoldbalt  48351  usgrexmpl12ngric  48608  pgnbgreunbgrlem2  48687  pgnbgreunbgrlem5  48693  ztprmneprm  48917  functermc  50077