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  1055  sbc2or  3738  eq0rdvALT  4349  rzalALT  4436  reusv2lem2  5342  po2ne  5555  poirr2  6088  sofld  6152  dfwe2  7728  tfindsg  7812  findsg  7848  omopth2  8519  swoord2  8677  unxpdomlem3  9168  preleqg  9536  suc11reg  9540  wemapwe  9618  r111  9699  r1pwss  9708  cflim2  10185  axunndlem1  10518  axunnd  10519  axpowndlem3  10522  axpownd  10524  axregndlem1  10525  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacndlem5  10534  axacnd  10535  fpwwe2lem12  10565  gchpwdom  10593  winalim2  10619  ltapr  10968  prodgt0  12002  squeeze0  12059  nnsub  12221  nn0sub  12487  elnnz  12534  nn0lt10b  12591  indstr2  12877  uzsupss  12890  nn01to3  12891  xrltnsym  13088  xrlttr  13091  qbtwnxr  13152  xltnegi  13168  xmullem  13216  xlemul1a  13240  xrsupsslem  13259  xrinfmsslem  13260  xrub  13264  xrsup0  13275  xrinf0  13291  reltxrnmnf  13295  ixxdisj  13313  icodisj  13429  fzm1  13561  addmodlteq  13908  facdiv  14249  hasheqf1oi  14313  relexpfld  15011  relexpuzrel  15014  reusq0  15427  climuni  15514  rlimno1  15616  sqrt2irr  16216  nn0rppwr  16530  prmdvdsexpr  16687  prmfac1  16690  dvdsprmpweqle  16857  ramlb  16990  ram0  16993  prmgaplem6  17027  prmlem1  17078  prmlem2  17090  pospo  18309  efgredlemc  19720  efgred  19723  ablsimpnosubgd  20081  sdrgacs  20778  prmirred  21454  psrvscafval  21927  fvmptnn04ifa  22815  fvmptnn04ifb  22816  fvmptnn04ifc  22817  fvmptnn04ifd  22818  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  0top  22948  pnfnei  23185  mnfnei  23186  cmpfi  23373  1stccnp  23427  filconn  23848  ivthlem2  25419  ivthlem3  25420  ovolicc2lem3  25486  itg1addlem4  25666  itg2seq  25709  dvcnvlem  25943  lhop2  25982  bpos1  27246  lgsdir2lem2  27289  lgsqrlem2  27310  lgseisenlem2  27339  2sqnn  27402  pntlem3  27572  ostth3  27601  nosupbnd1lem5  27676  noinfbnd1lem5  27691  noetasuplem4  27700  noetainflem4  27704  elnnzs  28393  expsne0  28428  tgcgr4  28599  axlowdimlem15  29025  nbusgrvtxm1  29448  wlkv0  29718  1to2vfriswmgr  30349  n4cyclfrgr  30361  frgrnbnb  30363  frgrregord013  30465  snsssng  32584  ifeqeqx  32612  rprmdvdsprod  33594  fldext2chn  33872  f1resrcmplf1dlem  35229  erdszelem4  35376  erdszelem8  35380  antnestlaw3lem  35872  finminlem  36500  nn0prpwlem  36504  nn0prpw  36505  ordcmp  36629  axtcond  36660  mh-setindnd  36719  iooelexlt  37678  relowlssretop  37679  smprngopr  38373  disjlem14  39222  prtlem14  39320  atltcvr  39881  dihord6apre  41702  dihord6b  41706  jm2.23  43424  onexlimgt  43671  ordnexbtwnsuc  43695  onov0suclim  43702  relexpmulg  44137  rzalf  45448  or2expropbi  47476  nnmul2  47772  icceuelpart  47890  iccpartnel  47892  poprelb  47978  goldbachthlem2  48003  fmtnoprmfac1  48022  fmtnoprmfac2  48024  fmtno4prmfac  48029  fmtno4prmfac193  48030  2pwp1prm  48046  lighneallem4  48067  requad1  48092  requad2  48093  evenprm2  48184  odd2prm2  48188  stgoldbwt  48246  sbgoldbwt  48247  sbgoldbalt  48251  usgrexmpl12ngric  48508  pgnbgreunbgrlem2  48587  pgnbgreunbgrlem5  48593  ztprmneprm  48817  functermc  49977