Theorem pm2.21d 122

Description: A contradiction implies anything. Deduction associated with pm2.21 124. (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 26	. 2 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))
3	2	con4d 116	1 ⊢ (𝜑 → (𝜓 → 𝜒))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.21ddALT  123  pm2.21  124  pm2.521g  175  prlem1  1070  sbc2or  3751  eq0rdvALT  4369  rzalALT  4454  reusv2lem2  5365  iunopeqop  5498  po2ne  5579  poirr2  6130  sofld  6191  f1resrcmplf1dlem  7301  dfwe2  7812  tfindsg  7896  findsg  7933  omopth2  8620  swoord2  8779  unxpdomlem3  9277  preleqg  9643  suc11reg  9647  wemapwe  9725  r111  9809  r1pwss  9818  cflim2  10368  axunndlem1  10707  axunnd  10708  axpowndlem3  10711  axpownd  10713  axregndlem1  10714  axregndlem2  10715  axinfndlem1  10717  axinfnd  10718  axacndlem1  10719  axacndlem2  10720  axacndlem3  10721  axacndlem4  10722  axacndlem5  10723  axacnd  10724  fpwwe2lem12  10754  gchpwdom  10782  winalim2  10808  ltapr  11157  prodgt0  12191  squeeze0  12247  nnsub  12409  nn0sub  12683  elnnz  12730  nn0lt10b  12788  indstr2  13081  uzsupss  13094  nn01to3  13095  xrltnsym  13293  xrlttr  13296  qbtwnxr  13357  xltnegi  13373  xmullem  13421  xlemul1a  13445  xrsupsslem  13464  xrinfmsslem  13465  xrub  13469  xrsup0  13480  xrinf0  13496  reltxrnmnf  13500  ixxdisj  13518  icodisj  13634  fzm1  13768  addmodlteq  14116  facdiv  14458  hasheqf1oi  14522  relexpfld  15231  relexpuzrel  15234  reusq0  15661  climuni  15748  rlimno1  15850  sqrt2irr  16446  nn0rppwr  16764  prmdvdsexpr  16922  prmfac1  16925  dvdsprmpweqle  17093  ramlb  17226  ram0  17229  prmgaplem6  17263  prmlem1  17314  prmlem2  17327  pospo  18546  efgredlemc  19989  efgred  19992  ablsimpnosubgd  20350  sdrgacs  21088  prmirred  21810  psrvscafval  22286  fvmptnn04ifa  23198  fvmptnn04ifb  23199  fvmptnn04ifc  23200  fvmptnn04ifd  23201  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  0top  23331  pnfnei  23568  mnfnei  23569  cmpfi  23756  1stccnp  23811  filconn  24232  ivthlem2  25803  ivthlem3  25804  ovolicc2lem3  25870  itg1addlem4  26050  itg2seq  26093  dvcnvlem  26326  lhop2  26365  bpos1  27640  lgsdir2lem2  27683  lgsqrlem2  27704  lgseisenlem2  27733  2sqnn  27796  pntlem3  27966  ostth3  27995  nosupbnd1lem5  28099  noinfbnd1lem5  28114  noetasuplem4  28123  noetainflem4  28127  elnnzs  28817  expsne0  28852  tgcgr4  29024  axlowdimlem15  29564  nbusgrvtxm1  29990  wlkv0  30260  1to2vfriswmgr  30910  n4cyclfrgr  30922  frgrnbnb  30924  frgrregord013  31026  snsssng  33182  ifeqeqx  33210  rprmdvdsprod  34136  fldext2chn  34430  j0ltaleph  36008  erdszelem4  36126  erdszelem8  36130  antnestlaw3lem  36622  finminlem  37284  nn0prpwlem  37288  nn0prpw  37289  ordcmp  37413  axtcond  37444  mh-setindnd  37503  iooelexlt  38477  relowlssretop  38478  smprngopr  39178  disjlem14  40025  prtlem14  40123  atltcvr  40684  dihord6apre  42505  dihord6b  42509  jm2.23  44196  onexlimgt  44437  ordnexbtwnsuc  44461  onov0suclim  44468  relexpmulg  44902  rzalf  46239  tmachlem-agreeprod  48152  or2expropbi  48309  aiotaexim  48373  nnmul2  48605  icceuelpart  48723  iccpartnel  48725  poprelb  48811  goldbachthlem2  48836  fmtnoprmfac1  48855  fmtnoprmfac2  48857  fmtno4prmfac  48862  fmtno4prmfac193  48863  2pwp1prm  48879  lighneallem4  48900  requad1  48925  requad2  48926  evenprm2  49017  odd2prm2  49021  stgoldbwt  49079  sbgoldbwt  49080  sbgoldbalt  49084  usgrexmpl12ngric  49341  pgnbgreunbgrlem2  49420  pgnbgreunbgrlem5  49426  smprngprmrng  49641  ztprmneprm  49664  functermc  50848