Theorem simp3 983

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.)

Assertion

Ref	Expression
simp3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Proof of Theorem simp3

Step	Hyp	Ref	Expression
1		3simpc 980	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜓 ∧ 𝜒))
2	1	simprd 113	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  simpl3  986  simpr3  989  simp3i  992  simp3d  995  simp13  1013  simp23  1016  simp33  1019  3anibar  1149  3ianorr  1287  stoic4a  1408  stoic4b  1409  mob2  2864  sotri2  4936  sotri3  4937  feq123  5264  resasplitss  5302  sefvex  5442  ftpg  5604  fsnunf  5620  fnfvima  5652  cocan1  5688  cocan2  5689  f1oiso2  5728  riotass  5757  moriotass  5758  ovmpox  5899  ovmpoga  5900  caovimo  5964  ofrval  5992  dfsmo2  6184  tfr1onlembfn  6241  tfrcllembfn  6254  freccllem  6299  frecfcllem  6301  frecsuclem  6303  frecrdg  6305  nnsucsssuc  6388  f1oen2g  6649  f1dom2g  6650  xpdom3m  6728  mapxpen  6742  diffifi  6788  unfidisj  6810  undifdc  6812  ssfidc  6823  sbthlemi9  6853  ctssdc  6998  endjudisj  7066  djuassen  7073  xpdjuen  7074  mulcanenq  7193  ltanqg  7208  addnnnq0  7257  nnanq0  7266  prltlu  7295  distrprg  7396  ltexprlemm  7408  recexprlem1ssl  7441  recexprlem1ssu  7442  addsrpr  7553  mulsrpr  7554  mulasssrg  7566  recexgt0sr  7581  ltpsrprg  7611  axmulass  7681  axpre-ltadd  7694  ltxrlt  7830  subadd2  7966  addsubass  7972  nppcan  7984  nppcan3  7986  subcan2  7987  subsub2  7990  subsub4  7995  pnpcan  8001  pnncan  8003  subcan  8017  subdi  8147  ltadd1  8191  leadd1  8192  leadd2  8193  ltsubadd  8194  ltsubadd2  8195  lesubadd  8196  lesubadd2  8197  ltaddsub  8198  leaddsub  8200  lesub1  8218  lesub2  8219  ltsub1  8220  ltsub2  8221  ltaddsublt  8333  gt0add  8335  reapadd1  8358  remulext1  8361  remulext2  8362  apadd2  8371  mulext2  8375  mulap0r  8377  leltap  8387  ltap  8395  apsub1  8404  divap0b  8443  divmulasscomap  8456  divcanap5  8474  dmdcanap  8482  redivclap  8491  div2negap  8495  lt2msq1  8643  ltdiv2  8645  nndivtr  8762  gtndiv  9146  eluzsub  9355  nn01to3  9409  qdivcl  9435  irrmul  9439  rpgecl  9470  divge1  9510  xaddass  9652  xltadd1  9659  ubioog  9697  ubioc1  9712  lbico1  9713  iccleub  9714  lbicc2  9767  ubicc2  9768  icoshftf1o  9774  fzen  9823  elfz1b  9870  uznfz  9883  elfzo0  9959  elfzo0z  9961  ubmelfzo  9977  fzonn0p1p1  9990  ubmelm1fzo  10003  qbtwnre  10034  flqwordi  10061  flltdivnn0lt  10077  ceiqle  10086  modqval  10097  modqvalr  10098  modqcl  10099  flqpmodeq  10100  modq0  10102  mulqmod0  10103  negqmod0  10104  modqge0  10105  modqlt  10106  modqdiffl  10108  modqdifz  10109  modqmulnn  10115  modqvalp1  10116  modqabs2  10131  modqmuladdnn0  10141  qnegmod  10142  addmodid  10145  modqeqmodmin  10167  modfzo0difsn  10168  addmodlteq  10171  frec2uzf1od  10179  expnegap0  10301  expgt1  10331  exprecap  10334  expaddzaplem  10336  expaddzap  10337  expmulzap  10339  mulbinom2  10408  expnbnd  10415  fihashss  10562  fimaxq  10573  seq3coll  10585  shftfibg  10592  redivap  10646  imdivap  10653  cjdivap  10681  maxleast  10985  lemininf  11005  ltmininf  11006  bdtrilem  11010  bdtri  11011  xrmaxaddlem  11029  xrmaxadd  11030  xrmineqinf  11038  xrltmininf  11039  xrminltinf  11041  xrminadd  11044  climuni  11062  reccn2ap  11082  isumz  11158  fsumsplitsnun  11188  geoisum1c  11289  prodfap0  11314  cos12dec  11474  summodnegmod  11524  dvdsmultr2  11533  mulmoddvds  11561  divalglemeuneg  11620  gcdaddm  11672  gcdass  11703  mulgcd  11704  gcddiv  11707  lcmass  11766  mulgcddvds  11775  qredeq  11777  congr  11781  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  prmexpb  11829  rpexp  11831  unennn  11910  fvsetsid  11993  ressid2  12018  ressval2  12019  rngmulrg  12077  basgen  12249  2basgeng  12251  ntrss  12288  neiss  12319  opnneiss  12327  restco  12343  restabs  12344  cnprcl2k  12375  cnpf2  12376  lmconst  12385  cnpnei  12388  cnptoprest  12408  cnmpt2t  12462  psmetsym  12498  psmetge0  12500  xmetge0  12534  xmetsym  12537  blvalps  12557  blval  12558  ssblps  12594  ssbl  12595  blpnfctr  12608  xmssym  12638  bdxmet  12670  metcnp3  12680  dvfvalap  12819  dvid  12831  dvcnp2cntop  12832  ptolemy  12905