Theorem pm2.21d 122

Description: A contradiction implies anything. Deduction associated with pm2.21 124. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	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  123  pm2.21  124  pm2.521g  175  prlem1  1068  sbc2or  3756  eq0rdvALT  4365  rzalALT  4452  reusv2lem2  5361  iunopeqop  5495  po2ne  5576  poirr2  6115  sofld  6177  dfwe2  7761  tfindsg  7845  findsg  7882  omopth2  8557  swoord2  8716  unxpdomlem3  9206  preleqg  9572  suc11reg  9576  wemapwe  9654  r111  9735  r1pwss  9744  cflim2  10235  axunndlem1  10568  axunnd  10569  axpowndlem3  10572  axpownd  10574  axregndlem1  10575  axregndlem2  10576  axinfndlem1  10578  axinfnd  10579  axacndlem1  10580  axacndlem2  10581  axacndlem3  10582  axacndlem4  10583  axacndlem5  10584  axacnd  10585  fpwwe2lem12  10615  gchpwdom  10643  winalim2  10669  ltapr  11018  prodgt0  12053  squeeze0  12109  nnsub  12271  nn0sub  12545  elnnz  12592  nn0lt10b  12649  indstr2  12942  uzsupss  12955  nn01to3  12956  xrltnsym  13153  xrlttr  13156  qbtwnxr  13217  xltnegi  13233  xmullem  13281  xlemul1a  13305  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  xrsup0  13340  xrinf0  13356  reltxrnmnf  13360  ixxdisj  13378  icodisj  13494  fzm1  13626  addmodlteq  13973  facdiv  14314  hasheqf1oi  14378  relexpfld  15076  relexpuzrel  15079  reusq0  15506  climuni  15593  rlimno1  15695  sqrt2irr  16295  nn0rppwr  16609  prmdvdsexpr  16766  prmfac1  16769  dvdsprmpweqle  16936  ramlb  17069  ram0  17072  prmgaplem6  17106  prmlem1  17157  prmlem2  17170  pospo  18389  efgredlemc  19806  efgred  19809  ablsimpnosubgd  20167  sdrgacs  20873  prmirred  21584  psrvscafval  22058  fvmptnn04ifa  22968  fvmptnn04ifb  22969  fvmptnn04ifc  22970  fvmptnn04ifd  22971  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  0top  23101  pnfnei  23338  mnfnei  23339  cmpfi  23526  1stccnp  23580  filconn  24001  ivthlem2  25572  ivthlem3  25573  ovolicc2lem3  25639  itg1addlem4  25819  itg2seq  25862  dvcnvlem  26096  lhop2  26135  bpos1  27405  lgsdir2lem2  27448  lgsqrlem2  27469  lgseisenlem2  27498  2sqnn  27561  pntlem3  27731  ostth3  27760  nosupbnd1lem5  27834  noinfbnd1lem5  27849  noetasuplem4  27858  noetainflem4  27862  elnnzs  28552  expsne0  28587  tgcgr4  28758  axlowdimlem15  29215  nbusgrvtxm1  29638  wlkv0  29908  1to2vfriswmgr  30539  n4cyclfrgr  30551  frgrnbnb  30553  frgrregord013  30655  snsssng  32770  ifeqeqx  32798  rprmdvdsprod  33741  fldext2chn  34035  f1resrcmplf1dlem  35390  erdszelem4  35557  erdszelem8  35561  antnestlaw3lem  36053  finminlem  36691  nn0prpwlem  36695  nn0prpw  36696  ordcmp  36820  axtcond  36851  mh-setindnd  36910  iooelexlt  37868  relowlssretop  37869  smprngopr  38563  disjlem14  39412  prtlem14  39510  atltcvr  40071  dihord6apre  41892  dihord6b  41896  jm2.23  43585  onexlimgt  43832  ordnexbtwnsuc  43856  onov0suclim  43863  relexpmulg  44298  rzalf  45595  or2expropbi  47626  nnmul2  47922  icceuelpart  48040  iccpartnel  48042  poprelb  48128  goldbachthlem2  48153  fmtnoprmfac1  48172  fmtnoprmfac2  48174  fmtno4prmfac  48179  fmtno4prmfac193  48180  2pwp1prm  48196  lighneallem4  48217  requad1  48242  requad2  48243  evenprm2  48334  odd2prm2  48338  stgoldbwt  48396  sbgoldbwt  48397  sbgoldbalt  48401  usgrexmpl12ngric  48658  pgnbgreunbgrlem2  48737  pgnbgreunbgrlem5  48743  smprngprmrng  48959  ztprmneprm  48978  functermc  50137