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  3315  sbcimdvOLD  3370  eq0rdv  3834  csbprcOLD  3836  rzal  3928  reusv2lem2  4694  reusv2lem2OLD  4695  poirr2  5330  sofld  5390  dfwe2  6754  tfindsg  6833  findsg  6866  omopth2  7431  swoord2  7541  unxpdomlem3  7931  suc11reg  8279  wemapwe  8357  r111  8401  r1pwss  8410  cflim2  8848  axunndlem1  9176  axunnd  9177  axpowndlem3  9180  axpownd  9182  axregndlem1  9183  axregndlem2  9184  axinfndlem1  9186  axinfnd  9187  axacndlem1  9188  axacndlem2  9189  axacndlem3  9190  axacndlem4  9191  axacndlem5  9192  axacnd  9193  fpwwe2lem13  9223  gchpwdom  9251  winalim2  9277  ltapr  9626  prodgt0  10621  squeeze0  10680  nnsub  10818  nn0sub  11102  elnnz  11132  nn0lt10b  11184  indstr2  11511  uzsupss  11526  nn01to3  11527  xrltnsym  11719  xrlttr  11722  qbtwnxr  11778  xltnegi  11794  xmullem  11837  xlemul1a  11861  xrsupsslem  11879  xrinfmsslem  11880  xrub  11884  xrsup0  11896  xrinf0  11910  reltxrnmnf  11916  ixxdisj  11934  icodisj  12041  fzm1  12161  addmodlteq  12479  facdiv  12808  hasheqf1oi  12871  hasheqf1oiOLD  12872  relexpfld  13500  relexpuzrel  13503  climuni  14001  rlimno1  14102  sqrt2irr  14690  prmdvdsexpr  15147  prmfac1  15149  dvdsprmpweqle  15316  ramlb  15449  ram0  15452  prmgaplem6  15486  prmlem1  15540  prmlem2  15553  pospo  16692  symgbas  17519  efgredlemc  17893  efgred  17896  psrvscafval  19119  prmirred  19572  fvmptnn04ifa  20381  fvmptnn04ifb  20382  fvmptnn04ifc  20383  fvmptnn04ifd  20384  chfacfscmulgsum  20391  chfacfpmmulgsum  20395  0top  20505  pnfnei  20741  mnfnei  20742  cmpfi  20928  1stccnp  20982  filcon  21404  ivthlem2  22907  ivthlem3  22908  ovolicc2lem3  22973  itg1addlem4  23151  itg2seq  23194  dvcnvlem  23422  lhop2  23461  bpos1  24701  lgsdir2lem2  24744  lgsqrlem2  24765  lgseisenlem2  24794  pntlem3  24991  ostth3  25020  tgcgr4  25120  axlowdimlem15  25530  uvtxisvtx  25760  uvtx01vtx  25762  wlkv0  26030  1to2vfriswmgra  26275  n4cyclfrgra  26287  frgranbnb  26289  frgrawopreg  26318  frgraregord013  26387  ifeqeqx  28537  erdszelem4  30279  erdszelem8  30283  finminlem  31321  nn0prpwlem  31325  nn0prpw  31326  ordcmp  31454  iooelexlt  32221  relowlssretop  32222  smprngopr  32915  prtlem14  33071  atltcvr  33633  dihord6apre  35457  dihord6b  35461  jm2.23  36475  sdrgacs  36691  rp-fakeimass  36777  relexpmulg  36922  rzalf  38100  icceuelpart  39886  iccpartnel  39888  goldbachthlem2  39908  fmtnoprmfac1  39927  fmtnoprmfac2  39929  fmtno4prmfac  39934  fmtno4prmfac193  39935  2pwp1prm  39953  lighneallem4  39977  evenprm2  40073  stgoldbwt  40110  bgoldbwt  40111  sgoldbalt  40115  nbusgrvtxm1  40716  1wlkv0  40968  1to2vfriswmgr  41558  n4cyclfrgr  41570  frgrnbnb  41572  frgrwopreg  41595  av-frgraregord013  41658  ztprmneprm  42027
  Copyright terms: Public domain W3C validator