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  8631  ackbij1lem16  10351  dvdsgcd  16761  coprimeprodsq  17030  pythagtriplem4  17041  pythagtriplem13  17049  pythagtriplem14  17050  pythagtriplem16  17052  pythagtrip  17056  lsmpropd  19942  matsc  22820  mdetunilem7  22988  smadiadetglem2  23042  m2cpminvid  23126  pmatcollpw1lem1  23147  mp2pm2mplem2  23180  isfil2  24230  filuni  24259  ufprim  24283  cxple2a  27084  isosctr  27206  nolesgn2o  28085  nogesgn1o  28087  sltstr  28230  cofcut2  28365  onsfi  28799  brbtwn2  29540  colinearalg  29545  ax5seg  29573  axcontlem4  29602  measres  34966  bayesth  35182  ofscom  36987  btwndiff  37007  ifscgr  37024  brofs2  37057  brifs2  37058  fscgr  37060  btwnconn1lem1  37067  btwnconn1lem2  37068  btwnconn1lem3  37069  btwnconn1lem4  37070  btwnconn1lem12  37078  seglecgr12im  37090  seglecgr12  37091  ivthALT  37338  islshpcv  40376  eqlkr  40422  lshpsmreu  40432  lshpkrlem5  40437  atlrelat1  40644  cvlcvr1  40662  cvlcvrp  40663  cvlatcvr1  40664  cvlatcvr2  40665  4noncolr3  40776  4noncolr2  40777  4noncolr1  40778  athgt  40779  3dimlem2  40782  3dimlem3a  40783  3dimlem4a  40786  3dimlem4  40787  3dimlem4OLDN  40788  3dim1  40790  3dim2  40791  hlatexch4  40804  ps-2b  40805  3atlem6  40811  llnnleat  40836  2atm  40850  ps-2c  40851  llnmlplnN  40862  2atmat  40884  2llnjN  40890  lvoli2  40904  4atlem3b  40921  4atlem10  40929  4atlem11a  40930  4atlem11b  40931  4atlem12a  40933  4atlem12b  40934  dalemswapyz  40979  lneq2at  41101  2lnat  41107  cdlema1N  41114  cdlemb  41117  pmodlem1  41169  llnmod2i2  41186  dalawlem1  41194  dalawlem3  41196  dalawlem4  41197  dalawlem6  41199  dalawlem9  41202  dalawlem10  41203  dalawlem11  41204  dalawlem12  41205  dalawlem13  41206  dalawlem15  41208  dalaw  41209  pclfinN  41223  osumcllem5N  41283  osumcllem6N  41284  osumcllem7N  41285  osumcllem9N  41287  osumcllem11N  41289  pl42lem1N  41302  lhp2at0  41355  lhp2atne  41357  lhp2at0ne  41359  4atexlem7  41398  ldilco  41439  ltrneq  41472  cdlemd2  41522  cdleme0ex2N  41547  cdleme7aa  41565  cdleme7c  41568  cdleme7d  41569  cdleme7ga  41571  cdleme11c  41584  cdleme11l  41592  cdleme11  41593  cdleme14  41596  cdleme15a  41597  cdleme15c  41599  cdleme16b  41602  cdleme16c  41603  cdleme16d  41604  cdleme16e  41605  cdleme16f  41606  cdleme0nex  41613  cdleme19b  41627  cdleme19d  41629  cdleme19e  41630  cdleme20f  41637  cdleme20k  41642  cdleme20l1  41643  cdleme20l2  41644  cdleme20l  41645  cdleme20m  41646  cdleme21a  41648  cdleme21b  41649  cdleme21c  41650  cdleme21ct  41652  cdleme21d  41653  cdleme21e  41654  cdleme21f  41655  cdleme21i  41658  cdleme22cN  41665  cdleme22eALTN  41668  cdleme25a  41676  cdleme25c  41678  cdleme25dN  41679  cdleme26e  41682  cdleme26ee  41683  cdleme26eALTN  41684  cdleme26f2ALTN  41687  cdleme26f2  41688  cdleme28a  41693  cdleme28b  41694  cdleme28  41696  cdlemefr32sn2aw  41727  cdlemefs32sn1aw  41737  cdleme43fsv1snlem  41743  cdleme41sn3a  41756  cdleme32c  41766  cdleme32e  41768  cdleme32le  41770  cdleme35a  41771  cdleme35b  41773  cdleme35d  41775  cdleme36a  41783  cdleme36m  41784  cdleme39a  41788  cdleme40m  41790  cdleme40n  41791  cdleme43bN  41813  cdleme43dN  41815  cdleme46f2g2  41816  cdleme46f2g1  41817  cdleme4gfv  41830  cdlemeg49le  41834  cdlemeg46c  41836  cdlemeg46fvaw  41839  cdlemeg46nlpq  41840  cdlemeg46gfre  41855  cdleme50trn2  41874  cdlemg2ce  41915  cdlemg2idN  41919  cdlemg7fvbwN  41930  cdlemg10bALTN  41959  cdlemg10a  41963  cdlemg12d  41969  cdlemg12g  41972  cdlemg12  41973  cdlemg13a  41974  cdlemg13  41975  cdlemg17b  41985  cdlemg17dN  41986  cdlemg17dALTN  41987  cdlemg17e  41988  cdlemg17pq  41995  cdlemg17bq  41996  cdlemg18d  42004  cdlemg19a  42006  cdlemg19  42007  cdlemg21  42009  cdlemg27a  42015  cdlemg31b0N  42017  cdlemg27b  42019  cdlemg31c  42022  cdlemg33b0  42024  cdlemg33c0  42025  cdlemg28b  42026  cdlemg33a  42029  cdlemg33  42034  ltrnco  42042  cdlemg44  42056  cdlemg47  42059  tendococl  42095  tendoplcl  42104  cdlemh1  42138  cdlemh2  42139  cdlemh  42140  cdlemi  42143  cdlemk5  42159  cdlemk6  42160  cdlemksel  42168  cdlemksv2  42170  cdlemk7  42171  cdlemk11  42172  cdlemk12  42173  cdlemkole  42176  cdlemk14  42177  cdlemk15  42178  cdlemk16a  42179  cdlemk16  42180  cdlemk1u  42182  cdlemk5u  42184  cdlemk6u  42185  cdlemkuel  42188  cdlemkuv2  42190  cdlemk18  42191  cdlemk19  42192  cdlemk7u  42193  cdlemk11u  42194  cdlemk12u  42195  cdlemk21N  42196  cdlemk20  42197  cdlemkoatnle-2N  42198  cdlemk13-2N  42199  cdlemkole-2N  42200  cdlemk14-2N  42201  cdlemk15-2N  42202  cdlemk16-2N  42203  cdlemk17-2N  42204  cdlemk18-2N  42209  cdlemk19-2N  42210  cdlemk7u-2N  42211  cdlemk11u-2N  42212  cdlemk12u-2N  42213  cdlemk21-2N  42214  cdlemk20-2N  42215  cdlemkuel-3  42221  cdlemkuv2-3N  42222  cdlemk22-3  42224  cdlemk33N  42232  cdlemk47  42272  cdlemk48  42273  cdlemk49  42274  cdlemk50  42275  cdlemk51  42276  cdlemk52  42277  cdlemk53a  42278  cdlemk55b  42283  cdlemkyyN  42285  cdlemk55u1  42288  cdlemk39u1  42290  cdlemk56  42294  dihord1  42541  dihord2a  42542  dihord10  42546  dihord11c  42547  dihord4  42581  dihord5apre  42585  dihglblem2N  42617  dihglbcpreN  42623  dihmeetlem3N  42628  dihjatc1  42634  dihjatc2N  42635  dihjatc3  42636  mapdpglem24  43027  baerlem3lem2  43033  baerlem5alem2  43034  baerlem5blem2  43035  hdmap14lem11  43201  hdmap14lem12  43202  hdmapglem7  43252  mzpsubst  44025  congmul  44240  congsub  44243  ntrclsiso  45328  ntrclskb  45330  ntrclsk3  45331  limsupre  46924  0ellimcdiv  46932  limclner  46934  sge0xaddlem2  47717  clnbgr3stgrgrlim  49390  gpgedgvtx1  49433  lincdifsn  49867  itschlc0yqe  50203  itscnhlc0xyqsol  50208