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  1031  prlem1  1055  sbc2or  3813  eq0rdvALT  4431  rzalALT  4533  reusv2lem2  5417  po2ne  5624  poirr2  6156  sofld  6218  dfwe2  7809  tfindsg  7898  findsg  7937  omopth2  8640  swoord2  8796  unxpdomlem3  9315  preleqg  9684  suc11reg  9688  wemapwe  9766  r111  9844  r1pwss  9853  cflim2  10332  axunndlem1  10664  axunnd  10665  axpowndlem3  10668  axpownd  10670  axregndlem1  10671  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem1  10676  axacndlem2  10677  axacndlem3  10678  axacndlem4  10679  axacndlem5  10680  axacnd  10681  fpwwe2lem12  10711  gchpwdom  10739  winalim2  10765  ltapr  11114  prodgt0  12141  squeeze0  12198  nnsub  12337  nn0sub  12603  elnnz  12649  nn0lt10b  12705  indstr2  12992  uzsupss  13005  nn01to3  13006  xrltnsym  13199  xrlttr  13202  qbtwnxr  13262  xltnegi  13278  xmullem  13326  xlemul1a  13350  xrsupsslem  13369  xrinfmsslem  13370  xrub  13374  xrsup0  13385  xrinf0  13400  reltxrnmnf  13404  ixxdisj  13422  icodisj  13536  fzm1  13664  addmodlteq  13997  facdiv  14336  hasheqf1oi  14400  relexpfld  15098  relexpuzrel  15101  reusq0  15511  climuni  15598  rlimno1  15702  sqrt2irr  16297  nn0rppwr  16608  prmdvdsexpr  16764  prmfac1  16767  dvdsprmpweqle  16933  ramlb  17066  ram0  17069  prmgaplem6  17103  prmlem1  17155  prmlem2  17167  pospo  18415  efgredlemc  19787  efgred  19790  ablsimpnosubgd  20148  sdrgacs  20824  prmirred  21508  psrvscafval  21991  fvmptnn04ifa  22877  fvmptnn04ifb  22878  fvmptnn04ifc  22879  fvmptnn04ifd  22880  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  0top  23011  pnfnei  23249  mnfnei  23250  cmpfi  23437  1stccnp  23491  filconn  23912  ivthlem2  25506  ivthlem3  25507  ovolicc2lem3  25573  itg1addlem4  25753  itg1addlem4OLD  25754  itg2seq  25797  dvcnvlem  26034  lhop2  26074  bpos1  27345  lgsdir2lem2  27388  lgsqrlem2  27409  lgseisenlem2  27438  2sqnn  27501  pntlem3  27671  ostth3  27700  nosupbnd1lem5  27775  noinfbnd1lem5  27790  noetasuplem4  27799  noetainflem4  27803  elnnzs  28405  expsne0  28432  tgcgr4  28557  axlowdimlem15  28989  nbusgrvtxm1  29414  wlkv0  29687  1to2vfriswmgr  30311  n4cyclfrgr  30323  frgrnbnb  30325  frgrregord013  30427  snsssng  32543  ifeqeqx  32565  rprmdvdsprod  33527  fldext2chn  33719  f1resrcmplf1dlem  35062  erdszelem4  35162  erdszelem8  35166  finminlem  36284  nn0prpwlem  36288  nn0prpw  36289  ordcmp  36413  iooelexlt  37328  relowlssretop  37329  smprngopr  38012  disjlem14  38754  prtlem14  38830  atltcvr  39392  dihord6apre  41213  dihord6b  41217  jm2.23  42953  onexlimgt  43204  ordnexbtwnsuc  43229  onov0suclim  43236  relexpmulg  43672  rzalf  44917  or2expropbi  46949  icceuelpart  47310  iccpartnel  47312  poprelb  47398  goldbachthlem2  47420  fmtnoprmfac1  47439  fmtnoprmfac2  47441  fmtno4prmfac  47446  fmtno4prmfac193  47447  2pwp1prm  47463  lighneallem4  47484  requad1  47496  requad2  47497  evenprm2  47588  odd2prm2  47592  stgoldbwt  47650  sbgoldbwt  47651  sbgoldbalt  47655  usgrexmpl12ngric  47853  ztprmneprm  48072