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  365  pm5.14  948  ecase2d  1000  prlem1  1025  sbc2or  3477  sbcimdvOLD  3532  eq0rdv  4012  csbprcOLD  4014  rzal  4106  reusv2lem2  4899  reusv2lem2OLD  4900  poirr2  5555  sofld  5616  dfwe2  7023  tfindsg  7102  findsg  7135  omopth2  7709  swoord2  7819  unxpdomlem3  8207  suc11reg  8554  wemapwe  8632  r111  8676  r1pwss  8685  cflim2  9123  axunndlem1  9455  axunnd  9456  axpowndlem3  9459  axpownd  9461  axregndlem1  9462  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacndlem5  9471  axacnd  9472  fpwwe2lem13  9502  gchpwdom  9530  winalim2  9556  ltapr  9905  prodgt0  10906  squeeze0  10964  nnsub  11097  nn0sub  11381  elnnz  11425  nn0lt10b  11477  indstr2  11805  uzsupss  11818  nn01to3  11819  xrltnsym  12008  xrlttr  12011  qbtwnxr  12069  xltnegi  12085  xmullem  12132  xlemul1a  12156  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  xrsup0  12191  xrinf0  12206  reltxrnmnf  12210  ixxdisj  12228  icodisj  12335  fzm1  12458  addmodlteq  12785  facdiv  13114  hasheqf1oi  13180  relexpfld  13833  relexpuzrel  13836  climuni  14327  rlimno1  14428  sqrt2irr  15023  prmdvdsexpr  15476  prmfac1  15478  dvdsprmpweqle  15637  ramlb  15770  ram0  15773  prmgaplem6  15807  prmlem1  15861  prmlem2  15874  pospo  17020  symgbas  17846  efgredlemc  18204  efgred  18207  psrvscafval  19438  prmirred  19891  fvmptnn04ifa  20703  fvmptnn04ifb  20704  fvmptnn04ifc  20705  fvmptnn04ifd  20706  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  0top  20835  pnfnei  21072  mnfnei  21073  cmpfi  21259  1stccnp  21313  filconn  21734  ivthlem2  23267  ivthlem3  23268  ovolicc2lem3  23333  itg1addlem4  23511  itg2seq  23554  dvcnvlem  23784  lhop2  23823  bpos1  25053  lgsdir2lem2  25096  lgsqrlem2  25117  lgseisenlem2  25146  pntlem3  25343  ostth3  25372  tgcgr4  25471  axlowdimlem15  25881  nbusgrvtxm1  26325  wlkv0  26603  1to2vfriswmgr  27259  n4cyclfrgr  27271  frgrnbnb  27273  frgrregord013  27382  ifeqeqx  29487  erdszelem4  31302  erdszelem8  31306  nosupbnd1lem5  31983  noetalem3  31990  finminlem  32437  nn0prpwlem  32442  nn0prpw  32443  ordcmp  32571  iooelexlt  33340  relowlssretop  33341  smprngopr  33981  prtlem14  34478  atltcvr  35039  dihord6apre  36862  dihord6b  36866  jm2.23  37880  sdrgacs  38088  rp-fakeimass  38174  relexpmulg  38319  rzalf  39490  icceuelpart  41697  iccpartnel  41699  goldbachthlem2  41783  fmtnoprmfac1  41802  fmtnoprmfac2  41804  fmtno4prmfac  41809  fmtno4prmfac193  41810  2pwp1prm  41828  lighneallem4  41852  evenprm2  41948  odd2prm2  41952  stgoldbwt  41989  sbgoldbwt  41990  sbgoldbalt  41994  ztprmneprm  42450
  Copyright terms: Public domain W3C validator