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  ecase2dOLD  1028  prlem1  1052  sbc2or  3785  eq0rdvALT  4407  rzalALT  4511  reusv2lem2  5401  po2ne  5608  poirr2  6133  sofld  6194  dfwe2  7780  tfindsg  7869  findsg  7909  omopth2  8609  swoord2  8761  unxpdomlem3  9281  preleqg  9644  suc11reg  9648  wemapwe  9726  r111  9804  r1pwss  9813  cflim2  10292  axunndlem1  10624  axunnd  10625  axpowndlem3  10628  axpownd  10630  axregndlem1  10631  axregndlem2  10632  axinfndlem1  10634  axinfnd  10635  axacndlem1  10636  axacndlem2  10637  axacndlem3  10638  axacndlem4  10639  axacndlem5  10640  axacnd  10641  fpwwe2lem12  10671  gchpwdom  10699  winalim2  10725  ltapr  11074  prodgt0  12097  squeeze0  12153  nnsub  12292  nn0sub  12558  elnnz  12604  nn0lt10b  12660  indstr2  12947  uzsupss  12960  nn01to3  12961  xrltnsym  13154  xrlttr  13157  qbtwnxr  13217  xltnegi  13233  xmullem  13281  xlemul1a  13305  xrsupsslem  13324  xrinfmsslem  13325  xrub  13329  xrsup0  13340  xrinf0  13355  reltxrnmnf  13359  ixxdisj  13377  icodisj  13491  fzm1  13619  addmodlteq  13949  facdiv  14284  hasheqf1oi  14348  relexpfld  15034  relexpuzrel  15037  reusq0  15447  climuni  15534  rlimno1  15638  sqrt2irr  16231  prmdvdsexpr  16693  prmfac1  16697  dvdsprmpweqle  16860  ramlb  16993  ram0  16996  prmgaplem6  17030  prmlem1  17082  prmlem2  17094  pospo  18342  efgredlemc  19705  efgred  19708  ablsimpnosubgd  20066  sdrgacs  20694  prmirred  21405  psrvscafval  21896  fvmptnn04ifa  22770  fvmptnn04ifb  22771  fvmptnn04ifc  22772  fvmptnn04ifd  22773  chfacfscmulgsum  22780  chfacfpmmulgsum  22784  0top  22904  pnfnei  23142  mnfnei  23143  cmpfi  23330  1stccnp  23384  filconn  23805  ivthlem2  25399  ivthlem3  25400  ovolicc2lem3  25466  itg1addlem4  25646  itg1addlem4OLD  25647  itg2seq  25690  dvcnvlem  25926  lhop2  25966  bpos1  27234  lgsdir2lem2  27277  lgsqrlem2  27298  lgseisenlem2  27327  2sqnn  27390  pntlem3  27560  ostth3  27589  nosupbnd1lem5  27663  noinfbnd1lem5  27678  noetasuplem4  27687  noetainflem4  27691  tgcgr4  28353  axlowdimlem15  28785  nbusgrvtxm1  29210  wlkv0  29483  1to2vfriswmgr  30107  n4cyclfrgr  30119  frgrnbnb  30121  frgrregord013  30223  snsssng  32328  ifeqeqx  32351  f1resrcmplf1dlem  34714  erdszelem4  34809  erdszelem8  34813  finminlem  35807  nn0prpwlem  35811  nn0prpw  35812  ordcmp  35936  iooelexlt  36846  relowlssretop  36847  smprngopr  37530  disjlem14  38274  prtlem14  38350  atltcvr  38912  dihord6apre  40733  dihord6b  40737  nn0rppwr  41896  jm2.23  42420  onexlimgt  42674  ordnexbtwnsuc  42699  onov0suclim  42706  relexpmulg  43143  rzalf  44382  or2expropbi  46418  icceuelpart  46778  iccpartnel  46780  poprelb  46866  goldbachthlem2  46888  fmtnoprmfac1  46907  fmtnoprmfac2  46909  fmtno4prmfac  46914  fmtno4prmfac193  46915  2pwp1prm  46931  lighneallem4  46952  requad1  46964  requad2  46965  evenprm2  47056  odd2prm2  47060  stgoldbwt  47118  sbgoldbwt  47119  sbgoldbalt  47123  ztprmneprm  47462