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 119
Description: A contradiction implies anything. Deduction associated with pm2.21 121. (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 115 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  120  pm2.21  121  2falsed  365  pm5.14  923  ecase2d  1016  prlem1  1041  sbc2or  3597  eq0rdv  4124  csbprcOLD  4126  rzal  4215  reusv2lem2  5000  poirr2  5662  sofld  5723  dfwe2  7129  tfindsg  7208  findsg  7241  omopth2  7819  swoord2  7929  unxpdomlem3  8323  preleqg  8675  suc11reg  8681  wemapwe  8759  r111  8803  r1pwss  8812  cflim2  9288  axunndlem1  9620  axunnd  9621  axpowndlem3  9624  axpownd  9626  axregndlem1  9627  axregndlem2  9628  axinfndlem1  9630  axinfnd  9631  axacndlem1  9632  axacndlem2  9633  axacndlem3  9634  axacndlem4  9635  axacndlem5  9636  axacnd  9637  fpwwe2lem13  9667  gchpwdom  9695  winalim2  9721  ltapr  10070  prodgt0  11071  squeeze0  11129  nnsub  11262  nn0sub  11546  elnnz  11590  nn0lt10b  11642  indstr2  11971  uzsupss  11984  nn01to3  11985  xrltnsym  12176  xrlttr  12179  qbtwnxr  12237  xltnegi  12253  xmullem  12300  xlemul1a  12324  xrsupsslem  12343  xrinfmsslem  12344  xrub  12348  xrsup0  12359  xrinf0  12374  reltxrnmnf  12378  ixxdisj  12396  icodisj  12505  fzm1  12628  addmodlteq  12954  facdiv  13279  hasheqf1oi  13345  relexpfld  13998  relexpuzrel  14001  climuni  14492  rlimno1  14593  sqrt2irr  15186  prmdvdsexpr  15637  prmfac1  15639  dvdsprmpweqle  15798  ramlb  15931  ram0  15934  prmgaplem6  15968  prmlem1  16022  prmlem2  16035  pospo  17182  symgbas  18008  efgredlemc  18366  efgred  18369  psrvscafval  19606  prmirred  20059  fvmptnn04ifa  20876  fvmptnn04ifb  20877  fvmptnn04ifc  20878  fvmptnn04ifd  20879  chfacfscmulgsum  20886  chfacfpmmulgsum  20890  0top  21009  pnfnei  21246  mnfnei  21247  cmpfi  21433  1stccnp  21487  filconn  21908  ivthlem2  23441  ivthlem3  23442  ovolicc2lem3  23508  itg1addlem4  23687  itg2seq  23730  dvcnvlem  23960  lhop2  23999  bpos1  25230  lgsdir2lem2  25273  lgsqrlem2  25294  lgseisenlem2  25323  pntlem3  25520  ostth3  25549  tgcgr4  25648  axlowdimlem15  26058  nbusgrvtxm1  26505  wlkv0  26783  1to2vfriswmgr  27462  n4cyclfrgr  27474  frgrnbnb  27476  frgrregord013  27595  ifeqeqx  29700  erdszelem4  31515  erdszelem8  31519  nosupbnd1lem5  32196  noetalem3  32203  finminlem  32650  nn0prpwlem  32655  nn0prpw  32656  ordcmp  32784  iooelexlt  33548  relowlssretop  33549  smprngopr  34184  prtlem14  34683  atltcvr  35244  dihord6apre  37067  dihord6b  37071  jm2.23  38090  sdrgacs  38298  rp-fakeimass  38384  relexpmulg  38529  rzalf  39699  icceuelpart  41901  iccpartnel  41903  goldbachthlem2  41987  fmtnoprmfac1  42006  fmtnoprmfac2  42008  fmtno4prmfac  42013  fmtno4prmfac193  42014  2pwp1prm  42032  lighneallem4  42056  evenprm2  42152  odd2prm2  42156  stgoldbwt  42193  sbgoldbwt  42194  sbgoldbalt  42198  ztprmneprm  42654
  Copyright terms: Public domain W3C validator