Theorem pm2.21d 121

Description: A contradiction implies anything. Deduction associated with pm2.21 123. (Contributed by NM, 10-Feb-1996.)

Hypothesis

Ref	Expression
pm2.21d.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
pm2.21d	⊢ (𝜑 → (𝜓 → 𝜒))

Proof of Theorem pm2.21d

Step	Hyp	Ref	Expression
1		pm2.21d.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2	1	a1d 25	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 115	1 ⊢ (𝜑 → (𝜓 → 𝜒))

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  122  pm2.21  123  pm2.521g  174  ecase2dOLD  1029  prlem1  1053  sbc2or  3784  eq0rdvALT  4401  rzalALT  4505  reusv2lem2  5393  po2ne  5600  poirr2  6124  sofld  6185  dfwe2  7770  tfindsg  7859  findsg  7899  omopth2  8598  swoord2  8750  unxpdomlem3  9270  preleqg  9632  suc11reg  9636  wemapwe  9714  r111  9792  r1pwss  9801  cflim2  10280  axunndlem1  10612  axunnd  10613  axpowndlem3  10616  axpownd  10618  axregndlem1  10619  axregndlem2  10620  axinfndlem1  10622  axinfnd  10623  axacndlem1  10624  axacndlem2  10625  axacndlem3  10626  axacndlem4  10627  axacndlem5  10628  axacnd  10629  fpwwe2lem12  10659  gchpwdom  10687  winalim2  10713  ltapr  11062  prodgt0  12085  squeeze0  12141  nnsub  12280  nn0sub  12546  elnnz  12592  nn0lt10b  12648  indstr2  12935  uzsupss  12948  nn01to3  12949  xrltnsym  13142  xrlttr  13145  qbtwnxr  13205  xltnegi  13221  xmullem  13269  xlemul1a  13293  xrsupsslem  13312  xrinfmsslem  13313  xrub  13317  xrsup0  13328  xrinf0  13343  reltxrnmnf  13347  ixxdisj  13365  icodisj  13479  fzm1  13607  addmodlteq  13937  facdiv  14272  hasheqf1oi  14336  relexpfld  15022  relexpuzrel  15025  reusq0  15435  climuni  15522  rlimno1  15626  sqrt2irr  16219  prmdvdsexpr  16681  prmfac1  16685  dvdsprmpweqle  16848  ramlb  16981  ram0  16984  prmgaplem6  17018  prmlem1  17070  prmlem2  17082  pospo  18330  efgredlemc  19693  efgred  19696  ablsimpnosubgd  20054  sdrgacs  20682  prmirred  21393  psrvscafval  21884  fvmptnn04ifa  22745  fvmptnn04ifb  22746  fvmptnn04ifc  22747  fvmptnn04ifd  22748  chfacfscmulgsum  22755  chfacfpmmulgsum  22759  0top  22879  pnfnei  23117  mnfnei  23118  cmpfi  23305  1stccnp  23359  filconn  23780  ivthlem2  25374  ivthlem3  25375  ovolicc2lem3  25441  itg1addlem4  25621  itg1addlem4OLD  25622  itg2seq  25665  dvcnvlem  25901  lhop2  25941  bpos1  27209  lgsdir2lem2  27252  lgsqrlem2  27273  lgseisenlem2  27302  2sqnn  27365  pntlem3  27535  ostth3  27564  nosupbnd1lem5  27638  noinfbnd1lem5  27653  noetasuplem4  27662  noetainflem4  27666  tgcgr4  28328  axlowdimlem15  28760  nbusgrvtxm1  29185  wlkv0  29458  1to2vfriswmgr  30082  n4cyclfrgr  30094  frgrnbnb  30096  frgrregord013  30198  snsssng  32303  ifeqeqx  32326  f1resrcmplf1dlem  34703  erdszelem4  34798  erdszelem8  34802  finminlem  35796  nn0prpwlem  35800  nn0prpw  35801  ordcmp  35925  iooelexlt  36835  relowlssretop  36836  smprngopr  37519  disjlem14  38264  prtlem14  38340  atltcvr  38902  dihord6apre  40723  dihord6b  40727  nn0rppwr  41887  jm2.23  42411  onexlimgt  42665  ordnexbtwnsuc  42690  onov0suclim  42697  relexpmulg  43134  rzalf  44373  or2expropbi  46410  icceuelpart  46770  iccpartnel  46772  poprelb  46858  goldbachthlem2  46880  fmtnoprmfac1  46899  fmtnoprmfac2  46901  fmtno4prmfac  46906  fmtno4prmfac193  46907  2pwp1prm  46923  lighneallem4  46944  requad1  46956  requad2  46957  evenprm2  47048  odd2prm2  47052  stgoldbwt  47110  sbgoldbwt  47111  sbgoldbalt  47115  ztprmneprm  47405

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »