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  1069  sbc2or  3752  eq0rdvALT  4372  rzalALT  4455  reusv2lem2  5369  iunopeqop  5503  po2ne  5584  poirr2  6123  sofld  6184  dfwe2  7771  tfindsg  7855  findsg  7892  omopth2  8567  swoord2  8726  unxpdomlem3  9216  preleqg  9582  suc11reg  9586  wemapwe  9664  r111  9745  r1pwss  9754  cflim2  10253  axunndlem1  10586  axunnd  10587  axpowndlem3  10590  axpownd  10592  axregndlem1  10593  axregndlem2  10594  axinfndlem1  10596  axinfnd  10597  axacndlem1  10598  axacndlem2  10599  axacndlem3  10600  axacndlem4  10601  axacndlem5  10602  axacnd  10603  fpwwe2lem12  10633  gchpwdom  10661  winalim2  10687  ltapr  11036  prodgt0  12068  squeeze0  12124  nnsub  12286  nn0sub  12560  elnnz  12607  nn0lt10b  12664  indstr2  12957  uzsupss  12970  nn01to3  12971  xrltnsym  13168  xrlttr  13171  qbtwnxr  13232  xltnegi  13248  xmullem  13296  xlemul1a  13320  xrsupsslem  13339  xrinfmsslem  13340  xrub  13344  xrsup0  13355  xrinf0  13371  reltxrnmnf  13375  ixxdisj  13393  icodisj  13509  fzm1  13642  addmodlteq  13989  facdiv  14330  hasheqf1oi  14394  relexpfld  15093  relexpuzrel  15096  reusq0  15523  climuni  15610  rlimno1  15712  sqrt2irr  16311  nn0rppwr  16625  prmdvdsexpr  16782  prmfac1  16785  dvdsprmpweqle  16952  ramlb  17085  ram0  17088  prmgaplem6  17122  prmlem1  17173  prmlem2  17186  pospo  18405  efgredlemc  19821  efgred  19824  ablsimpnosubgd  20182  sdrgacs  20915  prmirred  21635  psrvscafval  22109  fvmptnn04ifa  23018  fvmptnn04ifb  23019  fvmptnn04ifc  23020  fvmptnn04ifd  23021  chfacfscmulgsum  23028  chfacfpmmulgsum  23032  0top  23151  pnfnei  23388  mnfnei  23389  cmpfi  23576  1stccnp  23630  filconn  24051  ivthlem2  25622  ivthlem3  25623  ovolicc2lem3  25689  itg1addlem4  25869  itg2seq  25912  dvcnvlem  26146  lhop2  26185  bpos1  27458  lgsdir2lem2  27501  lgsqrlem2  27522  lgseisenlem2  27551  2sqnn  27614  pntlem3  27784  ostth3  27813  nosupbnd1lem5  27887  noinfbnd1lem5  27902  noetasuplem4  27911  noetainflem4  27915  elnnzs  28605  expsne0  28640  tgcgr4  28811  axlowdimlem15  29317  nbusgrvtxm1  29740  wlkv0  30010  1to2vfriswmgr  30641  n4cyclfrgr  30653  frgrnbnb  30655  frgrregord013  30757  snsssng  32871  ifeqeqx  32899  rprmdvdsprod  33833  fldext2chn  34127  f1resrcmplf1dlem  35483  erdszelem4  35694  erdszelem8  35698  antnestlaw3lem  36190  finminlem  36857  nn0prpwlem  36861  nn0prpw  36862  ordcmp  36986  axtcond  37017  mh-setindnd  37076  iooelexlt  38036  relowlssretop  38037  smprngopr  38731  disjlem14  39578  prtlem14  39676  atltcvr  40237  dihord6apre  42058  dihord6b  42062  jm2.23  43751  onexlimgt  43998  ordnexbtwnsuc  44022  onov0suclim  44029  relexpmulg  44464  rzalf  45765  or2expropbi  47799  nnmul2  48095  icceuelpart  48213  iccpartnel  48215  poprelb  48301  goldbachthlem2  48326  fmtnoprmfac1  48345  fmtnoprmfac2  48347  fmtno4prmfac  48352  fmtno4prmfac193  48353  2pwp1prm  48369  lighneallem4  48390  requad1  48415  requad2  48416  evenprm2  48507  odd2prm2  48511  stgoldbwt  48569  sbgoldbwt  48570  sbgoldbalt  48574  usgrexmpl12ngric  48831  pgnbgreunbgrlem2  48910  pgnbgreunbgrlem5  48916  smprngprmrng  49132  ztprmneprm  49155  functermc  50314