Theorem pm2.21d 118

Description: A contradiction implies anything. Deduction associated with pm2.21 120. (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 114	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  119  pm2.21  120  2falsed  366  pm5.14  930  ecase2d  981  prlem1  1005  sbc2or  3444  sbcimdvOLD  3499  eq0rdv  3979  csbprcOLD  3981  rzal  4073  reusv2lem2  4869  reusv2lem2OLD  4870  poirr2  5520  sofld  5581  dfwe2  6981  tfindsg  7060  findsg  7093  omopth2  7664  swoord2  7774  unxpdomlem3  8166  suc11reg  8516  wemapwe  8594  r111  8638  r1pwss  8647  cflim2  9085  axunndlem1  9417  axunnd  9418  axpowndlem3  9421  axpownd  9423  axregndlem1  9424  axregndlem2  9425  axinfndlem1  9427  axinfnd  9428  axacndlem1  9429  axacndlem2  9430  axacndlem3  9431  axacndlem4  9432  axacndlem5  9433  axacnd  9434  fpwwe2lem13  9464  gchpwdom  9492  winalim2  9518  ltapr  9867  prodgt0  10868  squeeze0  10926  nnsub  11059  nn0sub  11343  elnnz  11387  nn0lt10b  11439  indstr2  11767  uzsupss  11780  nn01to3  11781  xrltnsym  11970  xrlttr  11973  qbtwnxr  12031  xltnegi  12047  xmullem  12094  xlemul1a  12118  xrsupsslem  12137  xrinfmsslem  12138  xrub  12142  xrsup0  12153  xrinf0  12168  reltxrnmnf  12172  ixxdisj  12190  icodisj  12297  fzm1  12420  addmodlteq  12745  facdiv  13074  hasheqf1oi  13140  hasheqf1oiOLD  13141  relexpfld  13789  relexpuzrel  13792  climuni  14283  rlimno1  14384  sqrt2irr  14979  prmdvdsexpr  15429  prmfac1  15431  dvdsprmpweqle  15590  ramlb  15723  ram0  15726  prmgaplem6  15760  prmlem1  15814  prmlem2  15827  pospo  16973  symgbas  17800  efgredlemc  18158  efgred  18161  psrvscafval  19390  prmirred  19843  fvmptnn04ifa  20655  fvmptnn04ifb  20656  fvmptnn04ifc  20657  fvmptnn04ifd  20658  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  0top  20787  pnfnei  21024  mnfnei  21025  cmpfi  21211  1stccnp  21265  filconn  21687  ivthlem2  23221  ivthlem3  23222  ovolicc2lem3  23287  itg1addlem4  23466  itg2seq  23509  dvcnvlem  23739  lhop2  23778  bpos1  25008  lgsdir2lem2  25051  lgsqrlem2  25072  lgseisenlem2  25101  pntlem3  25298  ostth3  25327  tgcgr4  25426  axlowdimlem15  25836  nbusgrvtxm1  26281  wlkv0  26547  1to2vfriswmgr  27143  n4cyclfrgr  27155  frgrnbnb  27157  frgrregord013  27253  ifeqeqx  29361  erdszelem4  31176  erdszelem8  31180  nosupbnd1lem5  31858  noetalem3  31865  finminlem  32312  nn0prpwlem  32317  nn0prpw  32318  ordcmp  32446  iooelexlt  33210  relowlssretop  33211  smprngopr  33851  prtlem14  34159  atltcvr  34721  dihord6apre  36545  dihord6b  36549  jm2.23  37563  sdrgacs  37771  rp-fakeimass  37857  relexpmulg  38002  rzalf  39176  icceuelpart  41372  iccpartnel  41374  goldbachthlem2  41458  fmtnoprmfac1  41477  fmtnoprmfac2  41479  fmtno4prmfac  41484  fmtno4prmfac193  41485  2pwp1prm  41503  lighneallem4  41527  evenprm2  41623  odd2prm2  41627  stgoldbwt  41664  sbgoldbwt  41665  sbgoldbalt  41669  ztprmneprm  42125