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  3774  eq0rdvALT  4383  rzalALT  4485  reusv2lem2  5369  po2ne  5577  poirr2  6113  sofld  6176  dfwe2  7766  tfindsg  7854  findsg  7891  omopth2  8594  swoord2  8750  unxpdomlem3  9258  preleqg  9627  suc11reg  9631  wemapwe  9709  r111  9787  r1pwss  9796  cflim2  10275  axunndlem1  10607  axunnd  10608  axpowndlem3  10611  axpownd  10613  axregndlem1  10614  axregndlem2  10615  axinfndlem1  10617  axinfnd  10618  axacndlem1  10619  axacndlem2  10620  axacndlem3  10621  axacndlem4  10622  axacndlem5  10623  axacnd  10624  fpwwe2lem12  10654  gchpwdom  10682  winalim2  10708  ltapr  11057  prodgt0  12086  squeeze0  12143  nnsub  12282  nn0sub  12549  elnnz  12596  nn0lt10b  12653  indstr2  12941  uzsupss  12954  nn01to3  12955  xrltnsym  13151  xrlttr  13154  qbtwnxr  13214  xltnegi  13230  xmullem  13278  xlemul1a  13302  xrsupsslem  13321  xrinfmsslem  13322  xrub  13326  xrsup0  13337  xrinf0  13353  reltxrnmnf  13357  ixxdisj  13375  icodisj  13491  fzm1  13622  addmodlteq  13962  facdiv  14303  hasheqf1oi  14367  relexpfld  15066  relexpuzrel  15069  reusq0  15479  climuni  15566  rlimno1  15668  sqrt2irr  16265  nn0rppwr  16578  prmdvdsexpr  16734  prmfac1  16737  dvdsprmpweqle  16904  ramlb  17037  ram0  17040  prmgaplem6  17074  prmlem1  17125  prmlem2  17137  pospo  18353  efgredlemc  19724  efgred  19727  ablsimpnosubgd  20085  sdrgacs  20759  prmirred  21433  psrvscafval  21906  fvmptnn04ifa  22786  fvmptnn04ifb  22787  fvmptnn04ifc  22788  fvmptnn04ifd  22789  chfacfscmulgsum  22796  chfacfpmmulgsum  22800  0top  22919  pnfnei  23156  mnfnei  23157  cmpfi  23344  1stccnp  23398  filconn  23819  ivthlem2  25403  ivthlem3  25404  ovolicc2lem3  25470  itg1addlem4  25650  itg2seq  25693  dvcnvlem  25930  lhop2  25970  bpos1  27244  lgsdir2lem2  27287  lgsqrlem2  27308  lgseisenlem2  27337  2sqnn  27400  pntlem3  27570  ostth3  27599  nosupbnd1lem5  27674  noinfbnd1lem5  27689  noetasuplem4  27698  noetainflem4  27702  elnnzs  28304  expsne0  28331  tgcgr4  28456  axlowdimlem15  28881  nbusgrvtxm1  29304  wlkv0  29577  1to2vfriswmgr  30206  n4cyclfrgr  30218  frgrnbnb  30220  frgrregord013  30322  snsssng  32441  ifeqeqx  32469  rprmdvdsprod  33495  fldext2chn  33708  f1resrcmplf1dlem  35063  erdszelem4  35162  erdszelem8  35166  finminlem  36282  nn0prpwlem  36286  nn0prpw  36287  ordcmp  36411  iooelexlt  37326  relowlssretop  37327  smprngopr  38022  disjlem14  38762  prtlem14  38838  atltcvr  39400  dihord6apre  41221  dihord6b  41225  jm2.23  42967  onexlimgt  43214  ordnexbtwnsuc  43238  onov0suclim  43245  relexpmulg  43681  rzalf  44989  or2expropbi  47011  icceuelpart  47398  iccpartnel  47400  poprelb  47486  goldbachthlem2  47508  fmtnoprmfac1  47527  fmtnoprmfac2  47529  fmtno4prmfac  47534  fmtno4prmfac193  47535  2pwp1prm  47551  lighneallem4  47572  requad1  47584  requad2  47585  evenprm2  47676  odd2prm2  47680  stgoldbwt  47738  sbgoldbwt  47739  sbgoldbalt  47743  usgrexmpl12ngric  47990  ztprmneprm  48270  functermc  49341