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  5490  po2ne  5571  poirr2  6112  sofld  6174  f1resrcmplf1dlem  7266  dfwe2  7771  tfindsg  7855  findsg  7892  omopth2  8570  swoord2  8729  unxpdomlem3  9227  preleqg  9594  suc11reg  9598  wemapwe  9676  r111  9757  r1pwss  9766  cflim2  10313  axunndlem1  10652  axunnd  10653  axpowndlem3  10656  axpownd  10658  axregndlem1  10659  axregndlem2  10660  axinfndlem1  10662  axinfnd  10663  axacndlem1  10664  axacndlem2  10665  axacndlem3  10666  axacndlem4  10667  axacndlem5  10668  axacnd  10669  fpwwe2lem12  10699  gchpwdom  10727  winalim2  10753  ltapr  11102  prodgt0  12134  squeeze0  12190  nnsub  12352  nn0sub  12626  elnnz  12673  nn0lt10b  12731  indstr2  13024  uzsupss  13037  nn01to3  13038  xrltnsym  13236  xrlttr  13239  qbtwnxr  13300  xltnegi  13316  xmullem  13364  xlemul1a  13388  xrsupsslem  13407  xrinfmsslem  13408  xrub  13412  xrsup0  13423  xrinf0  13439  reltxrnmnf  13443  ixxdisj  13461  icodisj  13577  fzm1  13710  addmodlteq  14058  facdiv  14399  hasheqf1oi  14463  relexpfld  15170  relexpuzrel  15173  reusq0  15600  climuni  15687  rlimno1  15789  sqrt2irr  16385  nn0rppwr  16699  prmdvdsexpr  16856  prmfac1  16859  dvdsprmpweqle  17026  ramlb  17159  ram0  17162  prmgaplem6  17196  prmlem1  17247  prmlem2  17260  pospo  18479  efgredlemc  19921  efgred  19924  ablsimpnosubgd  20282  sdrgacs  21020  prmirred  21742  psrvscafval  22218  fvmptnn04ifa  23130  fvmptnn04ifb  23131  fvmptnn04ifc  23132  fvmptnn04ifd  23133  chfacfscmulgsum  23140  chfacfpmmulgsum  23144  0top  23263  pnfnei  23500  mnfnei  23501  cmpfi  23688  1stccnp  23743  filconn  24164  ivthlem2  25735  ivthlem3  25736  ovolicc2lem3  25802  itg1addlem4  25982  itg2seq  26025  dvcnvlem  26258  lhop2  26297  bpos1  27574  lgsdir2lem2  27617  lgsqrlem2  27638  lgseisenlem2  27667  2sqnn  27730  pntlem3  27900  ostth3  27929  nosupbnd1lem5  28003  noinfbnd1lem5  28018  noetasuplem4  28027  noetainflem4  28031  elnnzs  28721  expsne0  28756  tgcgr4  28928  axlowdimlem15  29468  nbusgrvtxm1  29894  wlkv0  30164  1to2vfriswmgr  30814  n4cyclfrgr  30826  frgrnbnb  30828  frgrregord013  30930  snsssng  33044  ifeqeqx  33072  rprmdvdsprod  34000  fldext2chn  34294  erdszelem4  35880  erdszelem8  35884  antnestlaw3lem  36376  finminlem  37028  nn0prpwlem  37032  nn0prpw  37033  ordcmp  37157  axtcond  37188  mh-setindnd  37247  iooelexlt  38205  relowlssretop  38206  smprngopr  38906  disjlem14  39753  prtlem14  39851  atltcvr  40412  dihord6apre  42233  dihord6b  42237  jm2.23  43941  onexlimgt  44188  ordnexbtwnsuc  44212  onov0suclim  44219  relexpmulg  44654  rzalf  45955  tmachlem-agreeprod  47869  or2expropbi  48026  nnmul2  48322  icceuelpart  48440  iccpartnel  48442  poprelb  48528  goldbachthlem2  48553  fmtnoprmfac1  48572  fmtnoprmfac2  48574  fmtno4prmfac  48579  fmtno4prmfac193  48580  2pwp1prm  48596  lighneallem4  48617  requad1  48642  requad2  48643  evenprm2  48734  odd2prm2  48738  stgoldbwt  48796  sbgoldbwt  48797  sbgoldbalt  48801  usgrexmpl12ngric  49058  pgnbgreunbgrlem2  49137  pgnbgreunbgrlem5  49143  smprngprmrng  49358  ztprmneprm  49381  functermc  50538