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  prlem1  1055  sbc2or  3751  eq0rdvALT  4362  rzalALT  4450  reusv2lem2  5346  po2ne  5556  poirr2  6089  sofld  6153  dfwe2  7729  tfindsg  7813  findsg  7849  omopth2  8521  swoord2  8679  unxpdomlem3  9170  preleqg  9536  suc11reg  9540  wemapwe  9618  r111  9699  r1pwss  9708  cflim2  10185  axunndlem1  10518  axunnd  10519  axpowndlem3  10522  axpownd  10524  axregndlem1  10525  axregndlem2  10526  axinfndlem1  10528  axinfnd  10529  axacndlem1  10530  axacndlem2  10531  axacndlem3  10532  axacndlem4  10533  axacndlem5  10534  axacnd  10535  fpwwe2lem12  10565  gchpwdom  10593  winalim2  10619  ltapr  10968  prodgt0  12000  squeeze0  12057  nnsub  12201  nn0sub  12463  elnnz  12510  nn0lt10b  12566  indstr2  12852  uzsupss  12865  nn01to3  12866  xrltnsym  13063  xrlttr  13066  qbtwnxr  13127  xltnegi  13143  xmullem  13191  xlemul1a  13215  xrsupsslem  13234  xrinfmsslem  13235  xrub  13239  xrsup0  13250  xrinf0  13266  reltxrnmnf  13270  ixxdisj  13288  icodisj  13404  fzm1  13535  addmodlteq  13881  facdiv  14222  hasheqf1oi  14286  relexpfld  14984  relexpuzrel  14987  reusq0  15400  climuni  15487  rlimno1  15589  sqrt2irr  16186  nn0rppwr  16500  prmdvdsexpr  16656  prmfac1  16659  dvdsprmpweqle  16826  ramlb  16959  ram0  16962  prmgaplem6  16996  prmlem1  17047  prmlem2  17059  pospo  18278  efgredlemc  19686  efgred  19689  ablsimpnosubgd  20047  sdrgacs  20746  prmirred  21441  psrvscafval  21916  fvmptnn04ifa  22806  fvmptnn04ifb  22807  fvmptnn04ifc  22808  fvmptnn04ifd  22809  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  0top  22939  pnfnei  23176  mnfnei  23177  cmpfi  23364  1stccnp  23418  filconn  23839  ivthlem2  25421  ivthlem3  25422  ovolicc2lem3  25488  itg1addlem4  25668  itg2seq  25711  dvcnvlem  25948  lhop2  25988  bpos1  27262  lgsdir2lem2  27305  lgsqrlem2  27326  lgseisenlem2  27355  2sqnn  27418  pntlem3  27588  ostth3  27617  nosupbnd1lem5  27692  noinfbnd1lem5  27707  noetasuplem4  27716  noetainflem4  27720  elnnzs  28409  expsne0  28444  tgcgr4  28615  axlowdimlem15  29041  nbusgrvtxm1  29464  wlkv0  29735  1to2vfriswmgr  30366  n4cyclfrgr  30378  frgrnbnb  30380  frgrregord013  30482  snsssng  32600  ifeqeqx  32628  rprmdvdsprod  33626  fldext2chn  33905  f1resrcmplf1dlem  35261  erdszelem4  35407  erdszelem8  35411  antnestlaw3lem  35903  finminlem  36531  nn0prpwlem  36535  nn0prpw  36536  ordcmp  36660  mh-setindnd  36686  iooelexlt  37606  relowlssretop  37607  smprngopr  38292  disjlem14  39141  prtlem14  39239  atltcvr  39800  dihord6apre  41621  dihord6b  41625  jm2.23  43342  onexlimgt  43589  ordnexbtwnsuc  43613  onov0suclim  43620  relexpmulg  44055  rzalf  45366  or2expropbi  47383  icceuelpart  47785  iccpartnel  47787  poprelb  47873  goldbachthlem2  47895  fmtnoprmfac1  47914  fmtnoprmfac2  47916  fmtno4prmfac  47921  fmtno4prmfac193  47922  2pwp1prm  47938  lighneallem4  47959  requad1  47971  requad2  47972  evenprm2  48063  odd2prm2  48067  stgoldbwt  48125  sbgoldbwt  48126  sbgoldbalt  48130  usgrexmpl12ngric  48387  pgnbgreunbgrlem2  48466  pgnbgreunbgrlem5  48472  ztprmneprm  48696  functermc  49856