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  176  2falsedOLD  380  ecase2d  1026  prlem1  1049  sbc2or  3783  eq0rdv  4359  rzal  4455  reusv2lem2  5302  po2ne  5491  poirr2  5986  sofld  6046  dfwe2  7498  tfindsg  7577  findsg  7611  omopth2  8212  swoord2  8323  unxpdomlem3  8726  preleqg  9080  suc11reg  9084  wemapwe  9162  r111  9206  r1pwss  9215  cflim2  9687  axunndlem1  10019  axunnd  10020  axpowndlem3  10023  axpownd  10025  axregndlem1  10026  axregndlem2  10027  axinfndlem1  10029  axinfnd  10030  axacndlem1  10031  axacndlem2  10032  axacndlem3  10033  axacndlem4  10034  axacndlem5  10035  axacnd  10036  fpwwe2lem13  10066  gchpwdom  10094  winalim2  10120  ltapr  10469  prodgt0  11489  squeeze0  11545  nnsub  11684  nn0sub  11950  elnnz  11994  nn0lt10b  12047  indstr2  12330  uzsupss  12343  nn01to3  12344  xrltnsym  12533  xrlttr  12536  qbtwnxr  12596  xltnegi  12612  xmullem  12660  xlemul1a  12684  xrsupsslem  12703  xrinfmsslem  12704  xrub  12708  xrsup0  12719  xrinf0  12734  reltxrnmnf  12738  ixxdisj  12756  icodisj  12865  fzm1  12990  addmodlteq  13317  facdiv  13650  hasheqf1oi  13715  relexpfld  14410  relexpuzrel  14413  reusq0  14824  climuni  14911  rlimno1  15012  sqrt2irr  15604  prmdvdsexpr  16063  prmfac1  16065  dvdsprmpweqle  16224  ramlb  16357  ram0  16360  prmgaplem6  16394  prmlem1  16443  prmlem2  16455  pospo  17585  efgredlemc  18873  efgred  18876  ablsimpnosubgd  19228  sdrgacs  19582  psrvscafval  20172  prmirred  20644  fvmptnn04ifa  21460  fvmptnn04ifb  21461  fvmptnn04ifc  21462  fvmptnn04ifd  21463  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  0top  21593  pnfnei  21830  mnfnei  21831  cmpfi  22018  1stccnp  22072  filconn  22493  ivthlem2  24055  ivthlem3  24056  ovolicc2lem3  24122  itg1addlem4  24302  itg2seq  24345  dvcnvlem  24575  lhop2  24614  bpos1  25861  lgsdir2lem2  25904  lgsqrlem2  25925  lgseisenlem2  25954  2sqnn  26017  pntlem3  26187  ostth3  26216  tgcgr4  26319  axlowdimlem15  26744  nbusgrvtxm1  27163  wlkv0  27434  1to2vfriswmgr  28060  n4cyclfrgr  28072  frgrnbnb  28074  frgrregord013  28176  ifeqeqx  30299  f1resrcmplf1dlem  32361  erdszelem4  32443  erdszelem8  32447  nosupbnd1lem5  33214  noetalem3  33221  finminlem  33668  nn0prpwlem  33672  nn0prpw  33673  ordcmp  33797  iooelexlt  34645  relowlssretop  34646  smprngopr  35332  prtlem14  36012  atltcvr  36573  dihord6apre  38394  dihord6b  38398  nn0rppwr  39189  jm2.23  39600  rp-fakeimass  39885  relexpmulg  40062  rzalf  41281  or2expropbi  43276  icceuelpart  43603  iccpartnel  43605  poprelb  43693  goldbachthlem2  43715  fmtnoprmfac1  43734  fmtnoprmfac2  43736  fmtno4prmfac  43741  fmtno4prmfac193  43742  2pwp1prm  43758  lighneallem4  43782  requad1  43794  requad2  43795  evenprm2  43886  odd2prm2  43890  stgoldbwt  43948  sbgoldbwt  43949  sbgoldbalt  43953  ztprmneprm  44402