Theorem simp13 1203

Description: Simplification of doubly triple conjunction. (Contributed by NM, 17-Nov-2011.)

Assertion

Ref	Expression
simp13	⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

Proof of Theorem simp13

Step	Hyp	Ref	Expression
1		simp3 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant1 1131	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 1085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  simp113  1302  simp213  1311  simp313  1320  omeu  8392  ackbij1lem16  9975  dvdsgcd  16233  coprimeprodsq  16490  pythagtriplem4  16501  pythagtriplem13  16509  pythagtriplem14  16510  pythagtriplem16  16512  pythagtrip  16516  lsmpropd  19264  matsc  21580  mdetunilem7  21748  smadiadetglem2  21802  m2cpminvid  21883  pmatcollpw1lem1  21904  mp2pm2mplem2  21937  isfil2  22988  filuni  23017  ufprim  23041  cxple2a  25835  isosctr  25952  brbtwn2  27254  colinearalg  27259  ax5seg  27287  axcontlem4  27316  measres  32169  bayesth  32385  nolesgn2o  33853  nogesgn1o  33855  sslttr  33980  cofcut2  34070  ofscom  34288  btwndiff  34308  ifscgr  34325  brofs2  34358  brifs2  34359  fscgr  34361  btwnconn1lem1  34368  btwnconn1lem2  34369  btwnconn1lem3  34370  btwnconn1lem4  34371  btwnconn1lem12  34379  seglecgr12im  34391  seglecgr12  34392  ivthALT  34503  islshpcv  37046  eqlkr  37092  lshpsmreu  37102  lshpkrlem5  37107  atlrelat1  37314  cvlcvr1  37332  cvlcvrp  37333  cvlatcvr1  37334  cvlatcvr2  37335  4noncolr3  37446  4noncolr2  37447  4noncolr1  37448  athgt  37449  3dimlem2  37452  3dimlem3a  37453  3dimlem4a  37456  3dimlem4  37457  3dimlem4OLDN  37458  3dim1  37460  3dim2  37461  hlatexch4  37474  ps-2b  37475  3atlem6  37481  llnnleat  37506  2atm  37520  ps-2c  37521  llnmlplnN  37532  2atmat  37554  2llnjN  37560  lvoli2  37574  4atlem3b  37591  4atlem10  37599  4atlem11a  37600  4atlem11b  37601  4atlem12a  37603  4atlem12b  37604  dalemswapyz  37649  lneq2at  37771  2lnat  37777  cdlema1N  37784  cdlemb  37787  pmodlem1  37839  llnmod2i2  37856  dalawlem1  37864  dalawlem3  37866  dalawlem4  37867  dalawlem6  37869  dalawlem9  37872  dalawlem10  37873  dalawlem11  37874  dalawlem12  37875  dalawlem13  37876  dalawlem15  37878  dalaw  37879  pclfinN  37893  osumcllem5N  37953  osumcllem6N  37954  osumcllem7N  37955  osumcllem9N  37957  osumcllem11N  37959  pl42lem1N  37972  lhp2at0  38025  lhp2atne  38027  lhp2at0ne  38029  4atexlem7  38068  ldilco  38109  ltrneq  38142  cdlemd2  38192  cdleme0ex2N  38217  cdleme7aa  38235  cdleme7c  38238  cdleme7d  38239  cdleme7ga  38241  cdleme11c  38254  cdleme11l  38262  cdleme11  38263  cdleme14  38266  cdleme15a  38267  cdleme15c  38269  cdleme16b  38272  cdleme16c  38273  cdleme16d  38274  cdleme16e  38275  cdleme16f  38276  cdleme0nex  38283  cdleme19b  38297  cdleme19d  38299  cdleme19e  38300  cdleme20f  38307  cdleme20k  38312  cdleme20l1  38313  cdleme20l2  38314  cdleme20l  38315  cdleme20m  38316  cdleme21a  38318  cdleme21b  38319  cdleme21c  38320  cdleme21ct  38322  cdleme21d  38323  cdleme21e  38324  cdleme21f  38325  cdleme21i  38328  cdleme22cN  38335  cdleme22eALTN  38338  cdleme25a  38346  cdleme25c  38348  cdleme25dN  38349  cdleme26e  38352  cdleme26ee  38353  cdleme26eALTN  38354  cdleme26f2ALTN  38357  cdleme26f2  38358  cdleme28a  38363  cdleme28b  38364  cdleme28  38366  cdlemefr32sn2aw  38397  cdlemefs32sn1aw  38407  cdleme43fsv1snlem  38413  cdleme41sn3a  38426  cdleme32c  38436  cdleme32e  38438  cdleme32le  38440  cdleme35a  38441  cdleme35b  38443  cdleme35d  38445  cdleme36a  38453  cdleme36m  38454  cdleme39a  38458  cdleme40m  38460  cdleme40n  38461  cdleme43bN  38483  cdleme43dN  38485  cdleme46f2g2  38486  cdleme46f2g1  38487  cdleme4gfv  38500  cdlemeg49le  38504  cdlemeg46c  38506  cdlemeg46fvaw  38509  cdlemeg46nlpq  38510  cdlemeg46gfre  38525  cdleme50trn2  38544  cdlemg2ce  38585  cdlemg2idN  38589  cdlemg7fvbwN  38600  cdlemg10bALTN  38629  cdlemg10a  38633  cdlemg12d  38639  cdlemg12g  38642  cdlemg12  38643  cdlemg13a  38644  cdlemg13  38645  cdlemg17b  38655  cdlemg17dN  38656  cdlemg17dALTN  38657  cdlemg17e  38658  cdlemg17pq  38665  cdlemg17bq  38666  cdlemg18d  38674  cdlemg19a  38676  cdlemg19  38677  cdlemg21  38679  cdlemg27a  38685  cdlemg31b0N  38687  cdlemg27b  38689  cdlemg31c  38692  cdlemg33b0  38694  cdlemg33c0  38695  cdlemg28b  38696  cdlemg33a  38699  cdlemg33  38704  ltrnco  38712  cdlemg44  38726  cdlemg47  38729  tendococl  38765  tendoplcl  38774  cdlemh1  38808  cdlemh2  38809  cdlemh  38810  cdlemi  38813  cdlemk5  38829  cdlemk6  38830  cdlemksel  38838  cdlemksv2  38840  cdlemk7  38841  cdlemk11  38842  cdlemk12  38843  cdlemkole  38846  cdlemk14  38847  cdlemk15  38848  cdlemk16a  38849  cdlemk16  38850  cdlemk1u  38852  cdlemk5u  38854  cdlemk6u  38855  cdlemkuel  38858  cdlemkuv2  38860  cdlemk18  38861  cdlemk19  38862  cdlemk7u  38863  cdlemk11u  38864  cdlemk12u  38865  cdlemk21N  38866  cdlemk20  38867  cdlemkoatnle-2N  38868  cdlemk13-2N  38869  cdlemkole-2N  38870  cdlemk14-2N  38871  cdlemk15-2N  38872  cdlemk16-2N  38873  cdlemk17-2N  38874  cdlemk18-2N  38879  cdlemk19-2N  38880  cdlemk7u-2N  38881  cdlemk11u-2N  38882  cdlemk12u-2N  38883  cdlemk21-2N  38884  cdlemk20-2N  38885  cdlemkuel-3  38891  cdlemkuv2-3N  38892  cdlemk22-3  38894  cdlemk33N  38902  cdlemk47  38942  cdlemk48  38943  cdlemk49  38944  cdlemk50  38945  cdlemk51  38946  cdlemk52  38947  cdlemk53a  38948  cdlemk55b  38953  cdlemkyyN  38955  cdlemk55u1  38958  cdlemk39u1  38960  cdlemk56  38964  dihord1  39211  dihord2a  39212  dihord10  39216  dihord11c  39217  dihord4  39251  dihord5apre  39255  dihglblem2N  39287  dihglbcpreN  39293  dihmeetlem3N  39298  dihjatc1  39304  dihjatc2N  39305  dihjatc3  39306  mapdpglem24  39697  baerlem3lem2  39703  baerlem5alem2  39704  baerlem5blem2  39705  hdmap14lem11  39871  hdmap14lem12  39872  hdmapglem7  39922  mzpsubst  40550  congmul  40769  congsub  40772  ntrclsiso  41630  ntrclskb  41632  ntrclsk3  41633  limsupre  43136  0ellimcdiv  43144  limclner  43146  sge0xaddlem2  43926  lincdifsn  45717  itschlc0yqe  46058  itscnhlc0xyqsol  46063