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 118
Description: A contradiction implies anything. Deduction associated with pm2.21 120. (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 114 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  119  pm2.21  120  2falsed  366  pm5.14  929  ecase2d  980  prlem1  1004  sbc2or  3438  sbcimdvOLD  3493  eq0rdv  3970  csbprcOLD  3972  rzal  4064  reusv2lem2  4860  reusv2lem2OLD  4861  poirr2  5508  sofld  5569  dfwe2  6966  tfindsg  7045  findsg  7078  omopth2  7649  swoord2  7759  unxpdomlem3  8151  suc11reg  8501  wemapwe  8579  r111  8623  r1pwss  8632  cflim2  9070  axunndlem1  9402  axunnd  9403  axpowndlem3  9406  axpownd  9408  axregndlem1  9409  axregndlem2  9410  axinfndlem1  9412  axinfnd  9413  axacndlem1  9414  axacndlem2  9415  axacndlem3  9416  axacndlem4  9417  axacndlem5  9418  axacnd  9419  fpwwe2lem13  9449  gchpwdom  9477  winalim2  9503  ltapr  9852  prodgt0  10853  squeeze0  10911  nnsub  11044  nn0sub  11328  elnnz  11372  nn0lt10b  11424  indstr2  11752  uzsupss  11765  nn01to3  11766  xrltnsym  11955  xrlttr  11958  qbtwnxr  12016  xltnegi  12032  xmullem  12079  xlemul1a  12103  xrsupsslem  12122  xrinfmsslem  12123  xrub  12127  xrsup0  12138  xrinf0  12153  reltxrnmnf  12157  ixxdisj  12175  icodisj  12282  fzm1  12404  addmodlteq  12728  facdiv  13057  hasheqf1oi  13123  hasheqf1oiOLD  13124  relexpfld  13770  relexpuzrel  13773  climuni  14264  rlimno1  14365  sqrt2irr  14960  prmdvdsexpr  15410  prmfac1  15412  dvdsprmpweqle  15571  ramlb  15704  ram0  15707  prmgaplem6  15741  prmlem1  15795  prmlem2  15808  pospo  16954  symgbas  17781  efgredlemc  18139  efgred  18142  psrvscafval  19371  prmirred  19824  fvmptnn04ifa  20636  fvmptnn04ifb  20637  fvmptnn04ifc  20638  fvmptnn04ifd  20639  chfacfscmulgsum  20646  chfacfpmmulgsum  20650  0top  20768  pnfnei  21005  mnfnei  21006  cmpfi  21192  1stccnp  21246  filconn  21668  ivthlem2  23202  ivthlem3  23203  ovolicc2lem3  23268  itg1addlem4  23447  itg2seq  23490  dvcnvlem  23720  lhop2  23759  bpos1  24989  lgsdir2lem2  25032  lgsqrlem2  25053  lgseisenlem2  25082  pntlem3  25279  ostth3  25308  tgcgr4  25407  axlowdimlem15  25817  nbusgrvtxm1  26262  wlkv0  26528  1to2vfriswmgr  27123  n4cyclfrgr  27135  frgrnbnb  27137  frgrregord013  27223  ifeqeqx  29333  erdszelem4  31150  erdszelem8  31154  nosupbnd1lem5  31832  noetalem3  31839  finminlem  32287  nn0prpwlem  32292  nn0prpw  32293  ordcmp  32421  iooelexlt  33181  relowlssretop  33182  smprngopr  33822  prtlem14  33978  atltcvr  34540  dihord6apre  36364  dihord6b  36368  jm2.23  37382  sdrgacs  37590  rp-fakeimass  37676  relexpmulg  37821  rzalf  38996  icceuelpart  41136  iccpartnel  41138  goldbachthlem2  41223  fmtnoprmfac1  41242  fmtnoprmfac2  41244  fmtno4prmfac  41249  fmtno4prmfac193  41250  2pwp1prm  41268  lighneallem4  41292  evenprm2  41388  odd2prm2  41392  stgoldbwt  41429  sbgoldbwt  41430  sbgoldbalt  41434  ztprmneprm  41890
  Copyright terms: Public domain W3C validator