Theorem pm2.21d 117

Description: A contradiction implies anything. Deduction associated with pm2.21 119. (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 113	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  118  pm2.21  119  2falsed  365  pm5.14  926  ecase2d  978  prlem1  997  sbc2or  3411  sbcimdvOLD  3466  eq0rdv  3931  csbprcOLD  3933  rzal  4025  reusv2lem2  4795  reusv2lem2OLD  4796  poirr2  5439  sofld  5500  dfwe2  6873  tfindsg  6952  findsg  6985  omopth2  7551  swoord2  7661  unxpdomlem3  8051  suc11reg  8399  wemapwe  8477  r111  8521  r1pwss  8530  cflim2  8968  axunndlem1  9296  axunnd  9297  axpowndlem3  9300  axpownd  9302  axregndlem1  9303  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacndlem5  9312  axacnd  9313  fpwwe2lem13  9343  gchpwdom  9371  winalim2  9397  ltapr  9746  prodgt0  10747  squeeze0  10805  nnsub  10936  nn0sub  11220  elnnz  11264  nn0lt10b  11316  indstr2  11643  uzsupss  11656  nn01to3  11657  xrltnsym  11846  xrlttr  11849  qbtwnxr  11905  xltnegi  11921  xmullem  11966  xlemul1a  11990  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  xrsup0  12025  xrinf0  12039  reltxrnmnf  12043  ixxdisj  12061  icodisj  12168  fzm1  12289  addmodlteq  12607  facdiv  12936  hasheqf1oi  13002  hasheqf1oiOLD  13003  relexpfld  13637  relexpuzrel  13640  climuni  14131  rlimno1  14232  sqrt2irr  14817  prmdvdsexpr  15267  prmfac1  15269  dvdsprmpweqle  15428  ramlb  15561  ram0  15564  prmgaplem6  15598  prmlem1  15652  prmlem2  15665  pospo  16796  symgbas  17623  efgredlemc  17981  efgred  17984  psrvscafval  19211  prmirred  19662  fvmptnn04ifa  20474  fvmptnn04ifb  20475  fvmptnn04ifc  20476  fvmptnn04ifd  20477  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  0top  20598  pnfnei  20834  mnfnei  20835  cmpfi  21021  1stccnp  21075  filcon  21497  ivthlem2  23028  ivthlem3  23029  ovolicc2lem3  23094  itg1addlem4  23272  itg2seq  23315  dvcnvlem  23543  lhop2  23582  bpos1  24808  lgsdir2lem2  24851  lgsqrlem2  24872  lgseisenlem2  24901  pntlem3  25098  ostth3  25127  tgcgr4  25226  axlowdimlem15  25636  uvtxisvtx  26018  uvtx01vtx  26020  wlkv0  26288  1to2vfriswmgra  26533  n4cyclfrgra  26545  frgranbnb  26547  frgrawopreg  26576  frgraregord013  26645  ifeqeqx  28745  erdszelem4  30430  erdszelem8  30434  finminlem  31482  nn0prpwlem  31487  nn0prpw  31488  ordcmp  31616  iooelexlt  32386  relowlssretop  32387  smprngopr  33021  prtlem14  33177  atltcvr  33739  dihord6apre  35563  dihord6b  35567  jm2.23  36581  sdrgacs  36790  rp-fakeimass  36876  relexpmulg  37021  rzalf  38199  icceuelpart  39974  iccpartnel  39976  goldbachthlem2  39996  fmtnoprmfac1  40015  fmtnoprmfac2  40017  fmtno4prmfac  40022  fmtno4prmfac193  40023  2pwp1prm  40041  lighneallem4  40065  evenprm2  40161  stgoldbwt  40198  bgoldbwt  40199  sgoldbalt  40203  nbusgrvtxm1  40607  1wlkv0  40859  1to2vfriswmgr  41449  n4cyclfrgr  41461  frgrnbnb  41463  frgrwopreg  41486  av-frgraregord013  41549  ztprmneprm  41918