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  3747  eq0rdvALT  4359  rzalALT  4461  reusv2lem2  5341  po2ne  5545  poirr2  6078  sofld  6142  dfwe2  7716  tfindsg  7800  findsg  7836  omopth2  8508  swoord2  8664  unxpdomlem3  9152  preleqg  9515  suc11reg  9519  wemapwe  9597  r111  9678  r1pwss  9687  cflim2  10164  axunndlem1  10496  axunnd  10497  axpowndlem3  10500  axpownd  10502  axregndlem1  10503  axregndlem2  10504  axinfndlem1  10506  axinfnd  10507  axacndlem1  10508  axacndlem2  10509  axacndlem3  10510  axacndlem4  10511  axacndlem5  10512  axacnd  10513  fpwwe2lem12  10543  gchpwdom  10571  winalim2  10597  ltapr  10946  prodgt0  11978  squeeze0  12035  nnsub  12179  nn0sub  12441  elnnz  12488  nn0lt10b  12545  indstr2  12835  uzsupss  12848  nn01to3  12849  xrltnsym  13046  xrlttr  13049  qbtwnxr  13109  xltnegi  13125  xmullem  13173  xlemul1a  13197  xrsupsslem  13216  xrinfmsslem  13217  xrub  13221  xrsup0  13232  xrinf0  13248  reltxrnmnf  13252  ixxdisj  13270  icodisj  13386  fzm1  13517  addmodlteq  13863  facdiv  14204  hasheqf1oi  14268  relexpfld  14966  relexpuzrel  14969  reusq0  15382  climuni  15469  rlimno1  15571  sqrt2irr  16168  nn0rppwr  16482  prmdvdsexpr  16638  prmfac1  16641  dvdsprmpweqle  16808  ramlb  16941  ram0  16944  prmgaplem6  16978  prmlem1  17029  prmlem2  17041  pospo  18259  efgredlemc  19667  efgred  19670  ablsimpnosubgd  20028  sdrgacs  20726  prmirred  21421  psrvscafval  21895  fvmptnn04ifa  22775  fvmptnn04ifb  22776  fvmptnn04ifc  22777  fvmptnn04ifd  22778  chfacfscmulgsum  22785  chfacfpmmulgsum  22789  0top  22908  pnfnei  23145  mnfnei  23146  cmpfi  23333  1stccnp  23387  filconn  23808  ivthlem2  25390  ivthlem3  25391  ovolicc2lem3  25457  itg1addlem4  25637  itg2seq  25680  dvcnvlem  25917  lhop2  25957  bpos1  27231  lgsdir2lem2  27274  lgsqrlem2  27295  lgseisenlem2  27324  2sqnn  27387  pntlem3  27557  ostth3  27586  nosupbnd1lem5  27661  noinfbnd1lem5  27676  noetasuplem4  27685  noetainflem4  27689  elnnzs  28335  expsne0  28369  tgcgr4  28519  axlowdimlem15  28945  nbusgrvtxm1  29368  wlkv0  29639  1to2vfriswmgr  30270  n4cyclfrgr  30282  frgrnbnb  30284  frgrregord013  30386  snsssng  32505  ifeqeqx  32533  rprmdvdsprod  33510  fldext2chn  33752  f1resrcmplf1dlem  35109  erdszelem4  35249  erdszelem8  35253  antnestlaw3lem  35745  finminlem  36373  nn0prpwlem  36377  nn0prpw  36378  ordcmp  36502  iooelexlt  37417  relowlssretop  37418  smprngopr  38102  disjlem14  38906  prtlem14  38983  atltcvr  39544  dihord6apre  41365  dihord6b  41369  jm2.23  43103  onexlimgt  43350  ordnexbtwnsuc  43374  onov0suclim  43381  relexpmulg  43817  rzalf  45128  or2expropbi  47148  icceuelpart  47550  iccpartnel  47552  poprelb  47638  goldbachthlem2  47660  fmtnoprmfac1  47679  fmtnoprmfac2  47681  fmtno4prmfac  47686  fmtno4prmfac193  47687  2pwp1prm  47703  lighneallem4  47724  requad1  47736  requad2  47737  evenprm2  47828  odd2prm2  47832  stgoldbwt  47890  sbgoldbwt  47891  sbgoldbalt  47895  usgrexmpl12ngric  48152  pgnbgreunbgrlem2  48231  pgnbgreunbgrlem5  48237  ztprmneprm  48461  functermc  49623