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  3779  eq0rdvALT  4388  rzalALT  4490  reusv2lem2  5379  po2ne  5588  poirr2  6124  sofld  6187  dfwe2  7776  tfindsg  7864  findsg  7901  omopth2  8604  swoord2  8760  unxpdomlem3  9270  preleqg  9637  suc11reg  9641  wemapwe  9719  r111  9797  r1pwss  9806  cflim2  10285  axunndlem1  10617  axunnd  10618  axpowndlem3  10621  axpownd  10623  axregndlem1  10624  axregndlem2  10625  axinfndlem1  10627  axinfnd  10628  axacndlem1  10629  axacndlem2  10630  axacndlem3  10631  axacndlem4  10632  axacndlem5  10633  axacnd  10634  fpwwe2lem12  10664  gchpwdom  10692  winalim2  10718  ltapr  11067  prodgt0  12096  squeeze0  12153  nnsub  12292  nn0sub  12559  elnnz  12606  nn0lt10b  12663  indstr2  12951  uzsupss  12964  nn01to3  12965  xrltnsym  13161  xrlttr  13164  qbtwnxr  13224  xltnegi  13240  xmullem  13288  xlemul1a  13312  xrsupsslem  13331  xrinfmsslem  13332  xrub  13336  xrsup0  13347  xrinf0  13362  reltxrnmnf  13366  ixxdisj  13384  icodisj  13498  fzm1  13629  addmodlteq  13969  facdiv  14309  hasheqf1oi  14373  relexpfld  15071  relexpuzrel  15074  reusq0  15484  climuni  15571  rlimno1  15673  sqrt2irr  16268  nn0rppwr  16581  prmdvdsexpr  16737  prmfac1  16740  dvdsprmpweqle  16907  ramlb  17040  ram0  17043  prmgaplem6  17077  prmlem1  17128  prmlem2  17140  pospo  18360  efgredlemc  19732  efgred  19735  ablsimpnosubgd  20093  sdrgacs  20771  prmirred  21448  psrvscafval  21923  fvmptnn04ifa  22805  fvmptnn04ifb  22806  fvmptnn04ifc  22807  fvmptnn04ifd  22808  chfacfscmulgsum  22815  chfacfpmmulgsum  22819  0top  22938  pnfnei  23175  mnfnei  23176  cmpfi  23363  1stccnp  23417  filconn  23838  ivthlem2  25424  ivthlem3  25425  ovolicc2lem3  25491  itg1addlem4  25671  itg2seq  25714  dvcnvlem  25951  lhop2  25991  bpos1  27264  lgsdir2lem2  27307  lgsqrlem2  27328  lgseisenlem2  27357  2sqnn  27420  pntlem3  27590  ostth3  27619  nosupbnd1lem5  27694  noinfbnd1lem5  27709  noetasuplem4  27718  noetainflem4  27722  elnnzs  28324  expsne0  28351  tgcgr4  28476  axlowdimlem15  28902  nbusgrvtxm1  29325  wlkv0  29598  1to2vfriswmgr  30227  n4cyclfrgr  30239  frgrnbnb  30241  frgrregord013  30343  snsssng  32462  ifeqeqx  32491  rprmdvdsprod  33502  fldext2chn  33713  f1resrcmplf1dlem  35075  erdszelem4  35174  erdszelem8  35178  finminlem  36294  nn0prpwlem  36298  nn0prpw  36299  ordcmp  36423  iooelexlt  37338  relowlssretop  37339  smprngopr  38034  disjlem14  38774  prtlem14  38850  atltcvr  39412  dihord6apre  41233  dihord6b  41237  jm2.23  42986  onexlimgt  43233  ordnexbtwnsuc  43257  onov0suclim  43264  relexpmulg  43700  rzalf  44994  or2expropbi  47019  icceuelpart  47396  iccpartnel  47398  poprelb  47484  goldbachthlem2  47506  fmtnoprmfac1  47525  fmtnoprmfac2  47527  fmtno4prmfac  47532  fmtno4prmfac193  47533  2pwp1prm  47549  lighneallem4  47570  requad1  47582  requad2  47583  evenprm2  47674  odd2prm2  47678  stgoldbwt  47736  sbgoldbwt  47737  sbgoldbalt  47741  usgrexmpl12ngric  47970  ztprmneprm  48236  functermc  49206