Theorem simp13 1224

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 1156	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	3ad2ant1 1151	1 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simp113  1323  simp213  1332  simp313  1341  omeu  8572  ackbij1lem16  10236  dvdsgcd  16634  coprimeprodsq  16900  pythagtriplem4  16911  pythagtriplem13  16919  pythagtriplem14  16920  pythagtriplem16  16922  pythagtrip  16926  lsmpropd  19804  matsc  22672  mdetunilem7  22840  smadiadetglem2  22894  m2cpminvid  22978  pmatcollpw1lem1  22999  mp2pm2mplem2  23032  isfil2  24082  filuni  24111  ufprim  24135  cxple2a  26936  isosctr  27058  nolesgn2o  27907  nogesgn1o  27909  sltstr  28052  cofcut2  28187  onsfi  28621  brbtwn2  29362  colinearalg  29367  ax5seg  29395  axcontlem4  29424  measres  34733  bayesth  34950  ofscom  36587  btwndiff  36607  ifscgr  36624  brofs2  36657  brifs2  36658  fscgr  36660  btwnconn1lem1  36667  btwnconn1lem2  36668  btwnconn1lem3  36669  btwnconn1lem4  36670  btwnconn1lem12  36678  seglecgr12im  36690  seglecgr12  36691  ivthALT  36954  islshpcv  39926  eqlkr  39972  lshpsmreu  39982  lshpkrlem5  39987  atlrelat1  40194  cvlcvr1  40212  cvlcvrp  40213  cvlatcvr1  40214  cvlatcvr2  40215  4noncolr3  40326  4noncolr2  40327  4noncolr1  40328  athgt  40329  3dimlem2  40332  3dimlem3a  40333  3dimlem4a  40336  3dimlem4  40337  3dimlem4OLDN  40338  3dim1  40340  3dim2  40341  hlatexch4  40354  ps-2b  40355  3atlem6  40361  llnnleat  40386  2atm  40400  ps-2c  40401  llnmlplnN  40412  2atmat  40434  2llnjN  40440  lvoli2  40454  4atlem3b  40471  4atlem10  40479  4atlem11a  40480  4atlem11b  40481  4atlem12a  40483  4atlem12b  40484  dalemswapyz  40529  lneq2at  40651  2lnat  40657  cdlema1N  40664  cdlemb  40667  pmodlem1  40719  llnmod2i2  40736  dalawlem1  40744  dalawlem3  40746  dalawlem4  40747  dalawlem6  40749  dalawlem9  40752  dalawlem10  40753  dalawlem11  40754  dalawlem12  40755  dalawlem13  40756  dalawlem15  40758  dalaw  40759  pclfinN  40773  osumcllem5N  40833  osumcllem6N  40834  osumcllem7N  40835  osumcllem9N  40837  osumcllem11N  40839  pl42lem1N  40852  lhp2at0  40905  lhp2atne  40907  lhp2at0ne  40909  4atexlem7  40948  ldilco  40989  ltrneq  41022  cdlemd2  41072  cdleme0ex2N  41097  cdleme7aa  41115  cdleme7c  41118  cdleme7d  41119  cdleme7ga  41121  cdleme11c  41134  cdleme11l  41142  cdleme11  41143  cdleme14  41146  cdleme15a  41147  cdleme15c  41149  cdleme16b  41152  cdleme16c  41153  cdleme16d  41154  cdleme16e  41155  cdleme16f  41156  cdleme0nex  41163  cdleme19b  41177  cdleme19d  41179  cdleme19e  41180  cdleme20f  41187  cdleme20k  41192  cdleme20l1  41193  cdleme20l2  41194  cdleme20l  41195  cdleme20m  41196  cdleme21a  41198  cdleme21b  41199  cdleme21c  41200  cdleme21ct  41202  cdleme21d  41203  cdleme21e  41204  cdleme21f  41205  cdleme21i  41208  cdleme22cN  41215  cdleme22eALTN  41218  cdleme25a  41226  cdleme25c  41228  cdleme25dN  41229  cdleme26e  41232  cdleme26ee  41233  cdleme26eALTN  41234  cdleme26f2ALTN  41237  cdleme26f2  41238  cdleme28a  41243  cdleme28b  41244  cdleme28  41246  cdlemefr32sn2aw  41277  cdlemefs32sn1aw  41287  cdleme43fsv1snlem  41293  cdleme41sn3a  41306  cdleme32c  41316  cdleme32e  41318  cdleme32le  41320  cdleme35a  41321  cdleme35b  41323  cdleme35d  41325  cdleme36a  41333  cdleme36m  41334  cdleme39a  41338  cdleme40m  41340  cdleme40n  41341  cdleme43bN  41363  cdleme43dN  41365  cdleme46f2g2  41366  cdleme46f2g1  41367  cdleme4gfv  41380  cdlemeg49le  41384  cdlemeg46c  41386  cdlemeg46fvaw  41389  cdlemeg46nlpq  41390  cdlemeg46gfre  41405  cdleme50trn2  41424  cdlemg2ce  41465  cdlemg2idN  41469  cdlemg7fvbwN  41480  cdlemg10bALTN  41509  cdlemg10a  41513  cdlemg12d  41519  cdlemg12g  41522  cdlemg12  41523  cdlemg13a  41524  cdlemg13  41525  cdlemg17b  41535  cdlemg17dN  41536  cdlemg17dALTN  41537  cdlemg17e  41538  cdlemg17pq  41545  cdlemg17bq  41546  cdlemg18d  41554  cdlemg19a  41556  cdlemg19  41557  cdlemg21  41559  cdlemg27a  41565  cdlemg31b0N  41567  cdlemg27b  41569  cdlemg31c  41572  cdlemg33b0  41574  cdlemg33c0  41575  cdlemg28b  41576  cdlemg33a  41579  cdlemg33  41584  ltrnco  41592  cdlemg44  41606  cdlemg47  41609  tendococl  41645  tendoplcl  41654  cdlemh1  41688  cdlemh2  41689  cdlemh  41690  cdlemi  41693  cdlemk5  41709  cdlemk6  41710  cdlemksel  41718  cdlemksv2  41720  cdlemk7  41721  cdlemk11  41722  cdlemk12  41723  cdlemkole  41726  cdlemk14  41727  cdlemk15  41728  cdlemk16a  41729  cdlemk16  41730  cdlemk1u  41732  cdlemk5u  41734  cdlemk6u  41735  cdlemkuel  41738  cdlemkuv2  41740  cdlemk18  41741  cdlemk19  41742  cdlemk7u  41743  cdlemk11u  41744  cdlemk12u  41745  cdlemk21N  41746  cdlemk20  41747  cdlemkoatnle-2N  41748  cdlemk13-2N  41749  cdlemkole-2N  41750  cdlemk14-2N  41751  cdlemk15-2N  41752  cdlemk16-2N  41753  cdlemk17-2N  41754  cdlemk18-2N  41759  cdlemk19-2N  41760  cdlemk7u-2N  41761  cdlemk11u-2N  41762  cdlemk12u-2N  41763  cdlemk21-2N  41764  cdlemk20-2N  41765  cdlemkuel-3  41771  cdlemkuv2-3N  41772  cdlemk22-3  41774  cdlemk33N  41782  cdlemk47  41822  cdlemk48  41823  cdlemk49  41824  cdlemk50  41825  cdlemk51  41826  cdlemk52  41827  cdlemk53a  41828  cdlemk55b  41833  cdlemkyyN  41835  cdlemk55u1  41838  cdlemk39u1  41840  cdlemk56  41844  dihord1  42091  dihord2a  42092  dihord10  42096  dihord11c  42097  dihord4  42131  dihord5apre  42135  dihglblem2N  42167  dihglbcpreN  42173  dihmeetlem3N  42178  dihjatc1  42184  dihjatc2N  42185  dihjatc3  42186  mapdpglem24  42577  baerlem3lem2  42583  baerlem5alem2  42584  baerlem5blem2  42585  hdmap14lem11  42751  hdmap14lem12  42752  hdmapglem7  42802  mzpsubst  43593  congmul  43808  congsub  43811  ntrclsiso  44907  ntrclskb  44909  ntrclsk3  44910  limsupre  46469  0ellimcdiv  46477  limclner  46479  sge0xaddlem2  47262  clnbgr3stgrgrlim  48935  gpgedgvtx1  48978  lincdifsn  49354  itschlc0yqe  49690  itscnhlc0xyqsol  49695