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  3748  eq0rdvALT  4356  rzalALT  4458  reusv2lem2  5335  po2ne  5538  poirr2  6068  sofld  6131  dfwe2  7702  tfindsg  7786  findsg  7822  omopth2  8494  swoord2  8650  unxpdomlem3  9137  preleqg  9500  suc11reg  9504  wemapwe  9582  r111  9660  r1pwss  9669  cflim2  10146  axunndlem1  10478  axunnd  10479  axpowndlem3  10482  axpownd  10484  axregndlem1  10485  axregndlem2  10486  axinfndlem1  10488  axinfnd  10489  axacndlem1  10490  axacndlem2  10491  axacndlem3  10492  axacndlem4  10493  axacndlem5  10494  axacnd  10495  fpwwe2lem12  10525  gchpwdom  10553  winalim2  10579  ltapr  10928  prodgt0  11960  squeeze0  12017  nnsub  12161  nn0sub  12423  elnnz  12470  nn0lt10b  12527  indstr2  12817  uzsupss  12830  nn01to3  12831  xrltnsym  13028  xrlttr  13031  qbtwnxr  13091  xltnegi  13107  xmullem  13155  xlemul1a  13179  xrsupsslem  13198  xrinfmsslem  13199  xrub  13203  xrsup0  13214  xrinf0  13230  reltxrnmnf  13234  ixxdisj  13252  icodisj  13368  fzm1  13499  addmodlteq  13845  facdiv  14186  hasheqf1oi  14250  relexpfld  14948  relexpuzrel  14951  reusq0  15364  climuni  15451  rlimno1  15553  sqrt2irr  16150  nn0rppwr  16464  prmdvdsexpr  16620  prmfac1  16623  dvdsprmpweqle  16790  ramlb  16923  ram0  16926  prmgaplem6  16960  prmlem1  17011  prmlem2  17023  pospo  18241  efgredlemc  19650  efgred  19653  ablsimpnosubgd  20011  sdrgacs  20709  prmirred  21404  psrvscafval  21878  fvmptnn04ifa  22758  fvmptnn04ifb  22759  fvmptnn04ifc  22760  fvmptnn04ifd  22761  chfacfscmulgsum  22768  chfacfpmmulgsum  22772  0top  22891  pnfnei  23128  mnfnei  23129  cmpfi  23316  1stccnp  23370  filconn  23791  ivthlem2  25373  ivthlem3  25374  ovolicc2lem3  25440  itg1addlem4  25620  itg2seq  25663  dvcnvlem  25900  lhop2  25940  bpos1  27214  lgsdir2lem2  27257  lgsqrlem2  27278  lgseisenlem2  27307  2sqnn  27370  pntlem3  27540  ostth3  27569  nosupbnd1lem5  27644  noinfbnd1lem5  27659  noetasuplem4  27668  noetainflem4  27672  elnnzs  28318  expsne0  28352  tgcgr4  28502  axlowdimlem15  28927  nbusgrvtxm1  29350  wlkv0  29621  1to2vfriswmgr  30249  n4cyclfrgr  30261  frgrnbnb  30263  frgrregord013  30365  snsssng  32484  ifeqeqx  32512  rprmdvdsprod  33489  fldext2chn  33731  f1resrcmplf1dlem  35088  erdszelem4  35206  erdszelem8  35210  antnestlaw3lem  35702  finminlem  36331  nn0prpwlem  36335  nn0prpw  36336  ordcmp  36460  iooelexlt  37375  relowlssretop  37376  smprngopr  38071  disjlem14  38815  prtlem14  38892  atltcvr  39453  dihord6apre  41274  dihord6b  41278  jm2.23  43008  onexlimgt  43255  ordnexbtwnsuc  43279  onov0suclim  43286  relexpmulg  43722  rzalf  45033  or2expropbi  47044  icceuelpart  47446  iccpartnel  47448  poprelb  47534  goldbachthlem2  47556  fmtnoprmfac1  47575  fmtnoprmfac2  47577  fmtno4prmfac  47582  fmtno4prmfac193  47583  2pwp1prm  47599  lighneallem4  47620  requad1  47632  requad2  47633  evenprm2  47724  odd2prm2  47728  stgoldbwt  47786  sbgoldbwt  47787  sbgoldbalt  47791  usgrexmpl12ngric  48048  pgnbgreunbgrlem2  48127  pgnbgreunbgrlem5  48133  ztprmneprm  48357  functermc  49519