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  prlem1  1054  sbc2or  3765  eq0rdvALT  4374  rzalALT  4476  reusv2lem2  5357  po2ne  5565  poirr2  6100  sofld  6163  dfwe2  7753  tfindsg  7840  findsg  7876  omopth2  8551  swoord2  8707  unxpdomlem3  9206  preleqg  9575  suc11reg  9579  wemapwe  9657  r111  9735  r1pwss  9744  cflim2  10223  axunndlem1  10555  axunnd  10556  axpowndlem3  10559  axpownd  10561  axregndlem1  10562  axregndlem2  10563  axinfndlem1  10565  axinfnd  10566  axacndlem1  10567  axacndlem2  10568  axacndlem3  10569  axacndlem4  10570  axacndlem5  10571  axacnd  10572  fpwwe2lem12  10602  gchpwdom  10630  winalim2  10656  ltapr  11005  prodgt0  12036  squeeze0  12093  nnsub  12237  nn0sub  12499  elnnz  12546  nn0lt10b  12603  indstr2  12893  uzsupss  12906  nn01to3  12907  xrltnsym  13104  xrlttr  13107  qbtwnxr  13167  xltnegi  13183  xmullem  13231  xlemul1a  13255  xrsupsslem  13274  xrinfmsslem  13275  xrub  13279  xrsup0  13290  xrinf0  13306  reltxrnmnf  13310  ixxdisj  13328  icodisj  13444  fzm1  13575  addmodlteq  13918  facdiv  14259  hasheqf1oi  14323  relexpfld  15022  relexpuzrel  15025  reusq0  15438  climuni  15525  rlimno1  15627  sqrt2irr  16224  nn0rppwr  16538  prmdvdsexpr  16694  prmfac1  16697  dvdsprmpweqle  16864  ramlb  16997  ram0  17000  prmgaplem6  17034  prmlem1  17085  prmlem2  17097  pospo  18311  efgredlemc  19682  efgred  19685  ablsimpnosubgd  20043  sdrgacs  20717  prmirred  21391  psrvscafval  21864  fvmptnn04ifa  22744  fvmptnn04ifb  22745  fvmptnn04ifc  22746  fvmptnn04ifd  22747  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  0top  22877  pnfnei  23114  mnfnei  23115  cmpfi  23302  1stccnp  23356  filconn  23777  ivthlem2  25360  ivthlem3  25361  ovolicc2lem3  25427  itg1addlem4  25607  itg2seq  25650  dvcnvlem  25887  lhop2  25927  bpos1  27201  lgsdir2lem2  27244  lgsqrlem2  27265  lgseisenlem2  27294  2sqnn  27357  pntlem3  27527  ostth3  27556  nosupbnd1lem5  27631  noinfbnd1lem5  27646  noetasuplem4  27655  noetainflem4  27659  elnnzs  28296  expsne0  28328  tgcgr4  28465  axlowdimlem15  28890  nbusgrvtxm1  29313  wlkv0  29586  1to2vfriswmgr  30215  n4cyclfrgr  30227  frgrnbnb  30229  frgrregord013  30331  snsssng  32450  ifeqeqx  32478  rprmdvdsprod  33512  fldext2chn  33725  f1resrcmplf1dlem  35083  erdszelem4  35188  erdszelem8  35192  antnestlaw3lem  35684  finminlem  36313  nn0prpwlem  36317  nn0prpw  36318  ordcmp  36442  iooelexlt  37357  relowlssretop  37358  smprngopr  38053  disjlem14  38797  prtlem14  38874  atltcvr  39436  dihord6apre  41257  dihord6b  41261  jm2.23  42992  onexlimgt  43239  ordnexbtwnsuc  43263  onov0suclim  43270  relexpmulg  43706  rzalf  45018  or2expropbi  47039  icceuelpart  47441  iccpartnel  47443  poprelb  47529  goldbachthlem2  47551  fmtnoprmfac1  47570  fmtnoprmfac2  47572  fmtno4prmfac  47577  fmtno4prmfac193  47578  2pwp1prm  47594  lighneallem4  47615  requad1  47627  requad2  47628  evenprm2  47719  odd2prm2  47723  stgoldbwt  47781  sbgoldbwt  47782  sbgoldbalt  47786  usgrexmpl12ngric  48033  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem5  48117  ztprmneprm  48339  functermc  49501