Theorem pm2.21d 122

Description: A contradiction implies anything. Deduction associated with pm2.21 124. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21ddALT  123  pm2.21  124  pm2.521g  175  prlem1  1070  sbc2or  3747  eq0rdvALT  4365  rzalALT  4450  reusv2lem2  5360  iunopeqop  5493  po2ne  5574  poirr2  6117  sofld  6178  f1resrcmplf1dlem  7278  dfwe2  7788  tfindsg  7872  findsg  7909  omopth2  8593  swoord2  8752  unxpdomlem3  9250  preleqg  9617  suc11reg  9621  wemapwe  9699  r111  9783  r1pwss  9792  cflim2  10342  axunndlem1  10681  axunnd  10682  axpowndlem3  10685  axpownd  10687  axregndlem1  10688  axregndlem2  10689  axinfndlem1  10691  axinfnd  10692  axacndlem1  10693  axacndlem2  10694  axacndlem3  10695  axacndlem4  10696  axacndlem5  10697  axacnd  10698  fpwwe2lem12  10728  gchpwdom  10756  winalim2  10782  ltapr  11131  prodgt0  12165  squeeze0  12221  nnsub  12383  nn0sub  12657  elnnz  12704  nn0lt10b  12762  indstr2  13055  uzsupss  13068  nn01to3  13069  xrltnsym  13267  xrlttr  13270  qbtwnxr  13331  xltnegi  13347  xmullem  13395  xlemul1a  13419  xrsupsslem  13438  xrinfmsslem  13439  xrub  13443  xrsup0  13454  xrinf0  13470  reltxrnmnf  13474  ixxdisj  13492  icodisj  13608  fzm1  13742  addmodlteq  14090  facdiv  14432  hasheqf1oi  14496  relexpfld  15203  relexpuzrel  15206  reusq0  15633  climuni  15720  rlimno1  15822  sqrt2irr  16418  nn0rppwr  16736  prmdvdsexpr  16894  prmfac1  16897  dvdsprmpweqle  17065  ramlb  17198  ram0  17201  prmgaplem6  17235  prmlem1  17286  prmlem2  17299  pospo  18518  efgredlemc  19960  efgred  19963  ablsimpnosubgd  20321  sdrgacs  21059  prmirred  21781  psrvscafval  22257  fvmptnn04ifa  23169  fvmptnn04ifb  23170  fvmptnn04ifc  23171  fvmptnn04ifd  23172  chfacfscmulgsum  23179  chfacfpmmulgsum  23183  0top  23302  pnfnei  23539  mnfnei  23540  cmpfi  23727  1stccnp  23782  filconn  24203  ivthlem2  25774  ivthlem3  25775  ovolicc2lem3  25841  itg1addlem4  26021  itg2seq  26064  dvcnvlem  26297  lhop2  26336  bpos1  27611  lgsdir2lem2  27654  lgsqrlem2  27675  lgseisenlem2  27704  2sqnn  27767  pntlem3  27937  ostth3  27966  nosupbnd1lem5  28070  noinfbnd1lem5  28085  noetasuplem4  28094  noetainflem4  28098  elnnzs  28788  expsne0  28823  tgcgr4  28995  axlowdimlem15  29535  nbusgrvtxm1  29961  wlkv0  30231  1to2vfriswmgr  30881  n4cyclfrgr  30893  frgrnbnb  30895  frgrregord013  30997  snsssng  33153  ifeqeqx  33181  rprmdvdsprod  34109  fldext2chn  34403  j0ltaleph  35940  erdszelem4  36028  erdszelem8  36032  antnestlaw3lem  36524  finminlem  37181  nn0prpwlem  37185  nn0prpw  37186  ordcmp  37310  axtcond  37341  mh-setindnd  37400  iooelexlt  38361  relowlssretop  38362  smprngopr  39062  disjlem14  39909  prtlem14  40007  atltcvr  40568  dihord6apre  42389  dihord6b  42393  jm2.23  44079  onexlimgt  44321  ordnexbtwnsuc  44345  onov0suclim  44352  relexpmulg  44786  rzalf  46110  tmachlem-agreeprod  48023  or2expropbi  48180  nnmul2  48476  icceuelpart  48594  iccpartnel  48596  poprelb  48682  goldbachthlem2  48707  fmtnoprmfac1  48726  fmtnoprmfac2  48728  fmtno4prmfac  48733  fmtno4prmfac193  48734  2pwp1prm  48750  lighneallem4  48771  requad1  48796  requad2  48797  evenprm2  48888  odd2prm2  48892  stgoldbwt  48950  sbgoldbwt  48951  sbgoldbalt  48955  usgrexmpl12ngric  49212  pgnbgreunbgrlem2  49291  pgnbgreunbgrlem5  49297  smprngprmrng  49512  ztprmneprm  49535  functermc  50692