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  177  2falsedOLD  381  ecase2d  1027  prlem1  1050  sbc2or  3707  eq0rdvALT  4304  rzalALT  4405  reusv2lem2  5272  po2ne  5462  poirr2  5961  sofld  6021  dfwe2  7501  tfindsg  7580  findsg  7615  omopth2  8226  swoord2  8337  unxpdomlem3  8775  preleqg  9124  suc11reg  9128  wemapwe  9206  r111  9250  r1pwss  9259  cflim2  9736  axunndlem1  10068  axunnd  10069  axpowndlem3  10072  axpownd  10074  axregndlem1  10075  axregndlem2  10076  axinfndlem1  10078  axinfnd  10079  axacndlem1  10080  axacndlem2  10081  axacndlem3  10082  axacndlem4  10083  axacndlem5  10084  axacnd  10085  fpwwe2lem12  10115  gchpwdom  10143  winalim2  10169  ltapr  10518  prodgt0  11538  squeeze0  11594  nnsub  11731  nn0sub  11997  elnnz  12043  nn0lt10b  12096  indstr2  12380  uzsupss  12393  nn01to3  12394  xrltnsym  12584  xrlttr  12587  qbtwnxr  12647  xltnegi  12663  xmullem  12711  xlemul1a  12735  xrsupsslem  12754  xrinfmsslem  12755  xrub  12759  xrsup0  12770  xrinf0  12785  reltxrnmnf  12789  ixxdisj  12807  icodisj  12921  fzm1  13049  addmodlteq  13376  facdiv  13710  hasheqf1oi  13775  relexpfld  14469  relexpuzrel  14472  reusq0  14883  climuni  14970  rlimno1  15071  sqrt2irr  15663  prmdvdsexpr  16127  prmfac1  16131  dvdsprmpweqle  16291  ramlb  16424  ram0  16427  prmgaplem6  16461  prmlem1  16513  prmlem2  16525  pospo  17663  efgredlemc  18952  efgred  18955  ablsimpnosubgd  19308  sdrgacs  19662  prmirred  20278  psrvscafval  20732  fvmptnn04ifa  21564  fvmptnn04ifb  21565  fvmptnn04ifc  21566  fvmptnn04ifd  21567  chfacfscmulgsum  21574  chfacfpmmulgsum  21578  0top  21697  pnfnei  21934  mnfnei  21935  cmpfi  22122  1stccnp  22176  filconn  22597  ivthlem2  24166  ivthlem3  24167  ovolicc2lem3  24233  itg1addlem4  24413  itg2seq  24456  dvcnvlem  24689  lhop2  24728  bpos1  25980  lgsdir2lem2  26023  lgsqrlem2  26044  lgseisenlem2  26073  2sqnn  26136  pntlem3  26306  ostth3  26335  tgcgr4  26438  axlowdimlem15  26863  nbusgrvtxm1  27282  wlkv0  27553  1to2vfriswmgr  28177  n4cyclfrgr  28189  frgrnbnb  28191  frgrregord013  28293  snsssng  30396  ifeqeqx  30421  f1resrcmplf1dlem  32591  erdszelem4  32685  erdszelem8  32689  nosupbnd1lem5  33513  noinfbnd1lem5  33528  noetasuplem4  33537  noetainflem4  33541  finminlem  34091  nn0prpwlem  34095  nn0prpw  34096  ordcmp  34220  iooelexlt  35094  relowlssretop  35095  smprngopr  35805  prtlem14  36485  atltcvr  37046  dihord6apre  38867  dihord6b  38871  nn0rppwr  39875  jm2.23  40355  rp-fakeimass  40638  relexpmulg  40829  rzalf  42064  or2expropbi  44037  icceuelpart  44380  iccpartnel  44382  poprelb  44468  goldbachthlem2  44490  fmtnoprmfac1  44509  fmtnoprmfac2  44511  fmtno4prmfac  44516  fmtno4prmfac193  44517  2pwp1prm  44533  lighneallem4  44554  requad1  44566  requad2  44567  evenprm2  44658  odd2prm2  44662  stgoldbwt  44720  sbgoldbwt  44721  sbgoldbalt  44725  ztprmneprm  45175