MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21d Structured version   Visualization version   GIF version

Theorem pm2.21d 116
Description: A contradiction implies anything. Deduction associated with pm2.21 118. (Contributed by NM, 10-Feb-1996.)
Hypothesis
Ref Expression
pm2.21d.1 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
pm2.21d (𝜑 → (𝜓𝜒))

Proof of Theorem pm2.21d
StepHypRef Expression
1 pm2.21d.1 . . 3 (𝜑 → ¬ 𝜓)
21a1d 25 . 2 (𝜑 → (¬ 𝜒 → ¬ 𝜓))
32con4d 112 1 (𝜑 → (𝜓𝜒))
Colors of variables: wff setvar class
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  117  pm2.21  118  2falsed  364  pm5.14  925  ecase2d  977  prlem1  996  sbc2or  3410  sbcimdvOLD  3465  eq0rdv  3930  csbprcOLD  3932  rzal  4024  reusv2lem2  4790  reusv2lem2OLD  4791  poirr2  5426  sofld  5486  dfwe2  6850  tfindsg  6929  findsg  6962  omopth2  7528  swoord2  7638  unxpdomlem3  8028  suc11reg  8376  wemapwe  8454  r111  8498  r1pwss  8507  cflim2  8945  axunndlem1  9273  axunnd  9274  axpowndlem3  9277  axpownd  9279  axregndlem1  9280  axregndlem2  9281  axinfndlem1  9283  axinfnd  9284  axacndlem1  9285  axacndlem2  9286  axacndlem3  9287  axacndlem4  9288  axacndlem5  9289  axacnd  9290  fpwwe2lem13  9320  gchpwdom  9348  winalim2  9374  ltapr  9723  prodgt0  10717  squeeze0  10775  nnsub  10906  nn0sub  11190  elnnz  11220  nn0lt10b  11272  indstr2  11599  uzsupss  11612  nn01to3  11613  xrltnsym  11805  xrlttr  11808  qbtwnxr  11864  xltnegi  11880  xmullem  11923  xlemul1a  11947  xrsupsslem  11965  xrinfmsslem  11966  xrub  11970  xrsup0  11981  xrinf0  11995  reltxrnmnf  11999  ixxdisj  12017  icodisj  12124  fzm1  12244  addmodlteq  12562  facdiv  12891  hasheqf1oi  12954  hasheqf1oiOLD  12955  relexpfld  13583  relexpuzrel  13586  climuni  14077  rlimno1  14178  sqrt2irr  14763  prmdvdsexpr  15213  prmfac1  15215  dvdsprmpweqle  15374  ramlb  15507  ram0  15510  prmgaplem6  15544  prmlem1  15598  prmlem2  15611  pospo  16742  symgbas  17569  efgredlemc  17927  efgred  17930  psrvscafval  19157  prmirred  19607  fvmptnn04ifa  20416  fvmptnn04ifb  20417  fvmptnn04ifc  20418  fvmptnn04ifd  20419  chfacfscmulgsum  20426  chfacfpmmulgsum  20430  0top  20540  pnfnei  20776  mnfnei  20777  cmpfi  20963  1stccnp  21017  filcon  21439  ivthlem2  22945  ivthlem3  22946  ovolicc2lem3  23011  itg1addlem4  23189  itg2seq  23232  dvcnvlem  23460  lhop2  23499  bpos1  24725  lgsdir2lem2  24768  lgsqrlem2  24789  lgseisenlem2  24818  pntlem3  25015  ostth3  25044  tgcgr4  25144  axlowdimlem15  25554  uvtxisvtx  25784  uvtx01vtx  25786  wlkv0  26054  1to2vfriswmgra  26299  n4cyclfrgra  26311  frgranbnb  26313  frgrawopreg  26342  frgraregord013  26411  ifeqeqx  28551  erdszelem4  30236  erdszelem8  30240  finminlem  31288  nn0prpwlem  31293  nn0prpw  31294  ordcmp  31422  iooelexlt  32189  relowlssretop  32190  smprngopr  32824  prtlem14  32980  atltcvr  33542  dihord6apre  35366  dihord6b  35370  jm2.23  36384  sdrgacs  36593  rp-fakeimass  36679  relexpmulg  36824  rzalf  38002  icceuelpart  39779  iccpartnel  39781  goldbachthlem2  39801  fmtnoprmfac1  39820  fmtnoprmfac2  39822  fmtno4prmfac  39827  fmtno4prmfac193  39828  2pwp1prm  39846  lighneallem4  39870  evenprm2  39966  stgoldbwt  40003  bgoldbwt  40004  sgoldbalt  40008  nbusgrvtxm1  40609  1wlkv0  40861  1to2vfriswmgr  41451  n4cyclfrgr  41463  frgrnbnb  41465  frgrwopreg  41488  av-frgraregord013  41551  ztprmneprm  41920
  Copyright terms: Public domain W3C validator