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  3431  sbcimdvOLD  3486  eq0rdv  3956  csbprcOLD  3958  rzal  4050  reusv2lem2  4834  reusv2lem2OLD  4835  poirr2  5483  sofld  5544  dfwe2  6929  tfindsg  7008  findsg  7041  omopth2  7610  swoord2  7720  unxpdomlem3  8111  suc11reg  8461  wemapwe  8539  r111  8583  r1pwss  8592  cflim2  9030  axunndlem1  9362  axunnd  9363  axpowndlem3  9366  axpownd  9368  axregndlem1  9369  axregndlem2  9370  axinfndlem1  9372  axinfnd  9373  axacndlem1  9374  axacndlem2  9375  axacndlem3  9376  axacndlem4  9377  axacndlem5  9378  axacnd  9379  fpwwe2lem13  9409  gchpwdom  9437  winalim2  9463  ltapr  9812  prodgt0  10813  squeeze0  10871  nnsub  11004  nn0sub  11288  elnnz  11332  nn0lt10b  11384  indstr2  11711  uzsupss  11724  nn01to3  11725  xrltnsym  11914  xrlttr  11917  qbtwnxr  11973  xltnegi  11989  xmullem  12034  xlemul1a  12058  xrsupsslem  12077  xrinfmsslem  12078  xrub  12082  xrsup0  12093  xrinf0  12107  reltxrnmnf  12111  ixxdisj  12129  icodisj  12236  fzm1  12358  addmodlteq  12682  facdiv  13011  hasheqf1oi  13077  hasheqf1oiOLD  13078  relexpfld  13718  relexpuzrel  13721  climuni  14212  rlimno1  14313  sqrt2irr  14898  prmdvdsexpr  15348  prmfac1  15350  dvdsprmpweqle  15509  ramlb  15642  ram0  15645  prmgaplem6  15679  prmlem1  15733  prmlem2  15746  pospo  16889  symgbas  17716  efgredlemc  18074  efgred  18077  psrvscafval  19304  prmirred  19757  fvmptnn04ifa  20569  fvmptnn04ifb  20570  fvmptnn04ifc  20571  fvmptnn04ifd  20572  chfacfscmulgsum  20579  chfacfpmmulgsum  20583  0top  20693  pnfnei  20929  mnfnei  20930  cmpfi  21116  1stccnp  21170  filconn  21592  ivthlem2  23123  ivthlem3  23124  ovolicc2lem3  23189  itg1addlem4  23367  itg2seq  23410  dvcnvlem  23638  lhop2  23677  bpos1  24903  lgsdir2lem2  24946  lgsqrlem2  24967  lgseisenlem2  24996  pntlem3  25193  ostth3  25222  tgcgr4  25321  axlowdimlem15  25731  nbusgrvtxm1  26162  wlkv0  26410  1to2vfriswmgr  27001  n4cyclfrgr  27013  frgrnbnb  27015  frgrwopreg  27038  frgrregord013  27101  ifeqeqx  29199  erdszelem4  30876  erdszelem8  30880  finminlem  31927  nn0prpwlem  31932  nn0prpw  31933  ordcmp  32061  iooelexlt  32815  relowlssretop  32816  smprngopr  33450  prtlem14  33606  atltcvr  34168  dihord6apre  35992  dihord6b  35996  jm2.23  37010  sdrgacs  37219  rp-fakeimass  37305  relexpmulg  37450  rzalf  38626  icceuelpart  40639  iccpartnel  40641  goldbachthlem2  40726  fmtnoprmfac1  40745  fmtnoprmfac2  40747  fmtno4prmfac  40752  fmtno4prmfac193  40753  2pwp1prm  40771  lighneallem4  40795  evenprm2  40891  stgoldbwt  40928  bgoldbwt  40929  sgoldbalt  40933  ztprmneprm  41367
  Copyright terms: Public domain W3C validator