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 111
Description: A contradiction implies anything. Deduction associated with pm2.21 113. (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 110 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  112  pm2.21  113  2falsed  360  pm5.14  916  ecase2d  968  prlem1  987  sbc2or  3300  sbcimdv  3353  eq0rdv  3809  csbprc  3810  rzal  3898  reusv2lem2  4644  poirr2  5274  sofld  5334  dfwe2  6685  tfindsg  6764  findsg  6797  omopth2  7362  swoord2  7472  unxpdomlem3  7862  suc11reg  8209  wemapwe  8287  r111  8331  r1pwss  8340  cflim2  8778  axunndlem1  9105  axunnd  9106  axpowndlem3  9109  axpownd  9111  axregndlem1  9112  axregndlem2  9113  axinfndlem1  9115  axinfnd  9116  axacndlem1  9117  axacndlem2  9118  axacndlem3  9119  axacndlem4  9120  axacndlem5  9121  axacnd  9122  fpwwe2lem13  9152  gchpwdom  9180  winalim2  9206  ltapr  9555  prodgt0  10539  squeeze0  10598  nnsub  10737  nn0sub  11011  elnnz  11038  nn0lt10b  11089  indstr2  11328  uzsupss  11347  nn01to3  11348  xrltnsym  11527  xrlttr  11530  qbtwnxr  11586  xltnegi  11602  xmullem  11645  xlemul1a  11669  xrsupsslem  11687  xrinfmsslem  11688  xrub  11692  xrsup0  11704  xrinf0  11718  xrinfm0OLD  11722  reltxrnmnf  11727  ixxdisj  11745  icodisj  11853  fzm1  11972  addmodlteq  12273  facdiv  12586  hasheqf1oi  12649  hasheqf1oiOLD  12650  relexpfld  13272  relexpuzrel  13275  climuni  13776  rlimno1  13877  sqrt2irr  14461  prmdvdsexpr  14831  prmfac1  14833  ramlb  15139  ram0  15142  prmgaplem6  15188  prmlem1  15240  prmlem2  15252  pospo  16384  symgbas  17182  efgredlemc  17556  efgred  17559  psrvscafval  18773  prmirred  19224  fvmptnn04ifa  20032  fvmptnn04ifb  20033  fvmptnn04ifc  20034  fvmptnn04ifd  20035  chfacfscmulgsum  20042  chfacfpmmulgsum  20046  0top  20156  pnfnei  20393  mnfnei  20394  cmpfi  20580  1stccnp  20634  filcon  21056  ivthlem2  22562  ivthlem3  22563  ovolicc2lem3  22631  itg1addlem4  22818  itg2seq  22861  dvcnvlem  23089  lhop2  23128  bpos1  24372  lgsdir2lem2  24413  lgsqrlem2  24431  lgseisenlem2  24439  pntlem3  24608  ostth3  24637  tgcgr4  24737  axlowdimlem15  25147  uvtxisvtx  25379  uvtx01vtx  25381  wlkv0  25649  1to2vfriswmgra  25894  n4cyclfrgra  25906  frgranbnb  25908  frgrawopreg  25937  frgraregord013  26006  ifeqeqx  28318  erdszelem4  30069  erdszelem8  30073  finminlem  31123  nn0prpwlem  31127  nn0prpw  31128  ordcmp  31256  iooelexlt  31986  relowlssretop  31987  smprngopr  32522  prtlem14  32679  atltcvr  33240  dihord6apre  35064  dihord6b  35068  jm2.23  36091  sdrgacs  36307  rp-fakeimass  36396  relexpmulg  36541  rzalf  37686  icceuelpart  39270  iccpartnel  39272  evenprm2  39362  stgoldbwt  39397  bgoldbwt  39398  sgoldbalt  39402  nbusgrvtxm1  40007  1wlkv0  40259  1to2vfriswmgr  40849  n4cyclfrgr  40861  frgrnbnb  40863  frgrwopreg  40886  av-frgraregord013  40949  ztprmneprm  41318
  Copyright terms: Public domain W3C validator