Theorem simp13 1198

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

Syntax hints:   → wi 4   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  simp113  1297  simp213  1306  simp313  1315  omeu  8066  ackbij1lem16  9508  dvdsgcd  15726  coprimeprodsq  15979  pythagtriplem4  15990  pythagtriplem13  15998  pythagtriplem14  15999  pythagtriplem16  16001  pythagtrip  16005  lsmpropd  18535  matsc  20748  mdetunilem7  20916  smadiadetglem2  20970  m2cpminvid  21050  pmatcollpw1lem1  21071  mp2pm2mplem2  21104  isfil2  22153  filuni  22182  ufprim  22206  cxple2a  24968  isosctr  25085  brbtwn2  26379  colinearalg  26384  ax5seg  26412  axcontlem4  26441  measres  31103  bayesth  31319  nolesgn2o  32793  ofscom  33083  btwndiff  33103  ifscgr  33120  brofs2  33153  brifs2  33154  fscgr  33156  btwnconn1lem1  33163  btwnconn1lem2  33164  btwnconn1lem3  33165  btwnconn1lem4  33166  btwnconn1lem12  33174  seglecgr12im  33186  seglecgr12  33187  ivthALT  33298  islshpcv  35745  eqlkr  35791  lshpsmreu  35801  lshpkrlem5  35806  atlrelat1  36013  cvlcvr1  36031  cvlcvrp  36032  cvlatcvr1  36033  cvlatcvr2  36034  4noncolr3  36145  4noncolr2  36146  4noncolr1  36147  athgt  36148  3dimlem2  36151  3dimlem3a  36152  3dimlem4a  36155  3dimlem4  36156  3dimlem4OLDN  36157  3dim1  36159  3dim2  36160  hlatexch4  36173  ps-2b  36174  3atlem6  36180  llnnleat  36205  2atm  36219  ps-2c  36220  llnmlplnN  36231  2atmat  36253  2llnjN  36259  lvoli2  36273  4atlem3b  36290  4atlem10  36298  4atlem11a  36299  4atlem11b  36300  4atlem12a  36302  4atlem12b  36303  dalemswapyz  36348  lneq2at  36470  2lnat  36476  cdlema1N  36483  cdlemb  36486  pmodlem1  36538  llnmod2i2  36555  dalawlem1  36563  dalawlem3  36565  dalawlem4  36566  dalawlem6  36568  dalawlem9  36571  dalawlem10  36572  dalawlem11  36573  dalawlem12  36574  dalawlem13  36575  dalawlem15  36577  dalaw  36578  pclfinN  36592  osumcllem5N  36652  osumcllem6N  36653  osumcllem7N  36654  osumcllem9N  36656  osumcllem11N  36658  pl42lem1N  36671  lhp2at0  36724  lhp2atne  36726  lhp2at0ne  36728  4atexlem7  36767  ldilco  36808  ltrneq  36841  cdlemd2  36891  cdleme0ex2N  36916  cdleme7aa  36934  cdleme7c  36937  cdleme7d  36938  cdleme7ga  36940  cdleme11c  36953  cdleme11l  36961  cdleme11  36962  cdleme14  36965  cdleme15a  36966  cdleme15c  36968  cdleme16b  36971  cdleme16c  36972  cdleme16d  36973  cdleme16e  36974  cdleme16f  36975  cdleme0nex  36982  cdleme19b  36996  cdleme19d  36998  cdleme19e  36999  cdleme20f  37006  cdleme20k  37011  cdleme20l1  37012  cdleme20l2  37013  cdleme20l  37014  cdleme20m  37015  cdleme21a  37017  cdleme21b  37018  cdleme21c  37019  cdleme21ct  37021  cdleme21d  37022  cdleme21e  37023  cdleme21f  37024  cdleme21i  37027  cdleme22cN  37034  cdleme22eALTN  37037  cdleme25a  37045  cdleme25c  37047  cdleme25dN  37048  cdleme26e  37051  cdleme26ee  37052  cdleme26eALTN  37053  cdleme26f2ALTN  37056  cdleme26f2  37057  cdleme28a  37062  cdleme28b  37063  cdleme28  37065  cdlemefr32sn2aw  37096  cdlemefs32sn1aw  37106  cdleme43fsv1snlem  37112  cdleme41sn3a  37125  cdleme32c  37135  cdleme32e  37137  cdleme32le  37139  cdleme35a  37140  cdleme35b  37142  cdleme35d  37144  cdleme36a  37152  cdleme36m  37153  cdleme39a  37157  cdleme40m  37159  cdleme40n  37160  cdleme43bN  37182  cdleme43dN  37184  cdleme46f2g2  37185  cdleme46f2g1  37186  cdleme4gfv  37199  cdlemeg49le  37203  cdlemeg46c  37205  cdlemeg46fvaw  37208  cdlemeg46nlpq  37209  cdlemeg46gfre  37224  cdleme50trn2  37243  cdlemg2ce  37284  cdlemg2idN  37288  cdlemg7fvbwN  37299  cdlemg10bALTN  37328  cdlemg10a  37332  cdlemg12d  37338  cdlemg12g  37341  cdlemg12  37342  cdlemg13a  37343  cdlemg13  37344  cdlemg17b  37354  cdlemg17dN  37355  cdlemg17dALTN  37356  cdlemg17e  37357  cdlemg17pq  37364  cdlemg17bq  37365  cdlemg18d  37373  cdlemg19a  37375  cdlemg19  37376  cdlemg21  37378  cdlemg27a  37384  cdlemg31b0N  37386  cdlemg27b  37388  cdlemg31c  37391  cdlemg33b0  37393  cdlemg33c0  37394  cdlemg28b  37395  cdlemg33a  37398  cdlemg33  37403  ltrnco  37411  cdlemg44  37425  cdlemg47  37428  tendococl  37464  tendoplcl  37473  cdlemh1  37507  cdlemh2  37508  cdlemh  37509  cdlemi  37512  cdlemk5  37528  cdlemk6  37529  cdlemksel  37537  cdlemksv2  37539  cdlemk7  37540  cdlemk11  37541  cdlemk12  37542  cdlemkole  37545  cdlemk14  37546  cdlemk15  37547  cdlemk16a  37548  cdlemk16  37549  cdlemk1u  37551  cdlemk5u  37553  cdlemk6u  37554  cdlemkuel  37557  cdlemkuv2  37559  cdlemk18  37560  cdlemk19  37561  cdlemk7u  37562  cdlemk11u  37563  cdlemk12u  37564  cdlemk21N  37565  cdlemk20  37566  cdlemkoatnle-2N  37567  cdlemk13-2N  37568  cdlemkole-2N  37569  cdlemk14-2N  37570  cdlemk15-2N  37571  cdlemk16-2N  37572  cdlemk17-2N  37573  cdlemk18-2N  37578  cdlemk19-2N  37579  cdlemk7u-2N  37580  cdlemk11u-2N  37581  cdlemk12u-2N  37582  cdlemk21-2N  37583  cdlemk20-2N  37584  cdlemkuel-3  37590  cdlemkuv2-3N  37591  cdlemk22-3  37593  cdlemk33N  37601  cdlemk47  37641  cdlemk48  37642  cdlemk49  37643  cdlemk50  37644  cdlemk51  37645  cdlemk52  37646  cdlemk53a  37647  cdlemk55b  37652  cdlemkyyN  37654  cdlemk55u1  37657  cdlemk39u1  37659  cdlemk56  37663  dihord1  37910  dihord2a  37911  dihord10  37915  dihord11c  37916  dihord4  37950  dihord5apre  37954  dihglblem2N  37986  dihglbcpreN  37992  dihmeetlem3N  37997  dihjatc1  38003  dihjatc2N  38004  dihjatc3  38005  mapdpglem24  38396  baerlem3lem2  38402  baerlem5alem2  38403  baerlem5blem2  38404  hdmap14lem11  38570  hdmap14lem12  38571  hdmapglem7  38621  mzpsubst  38855  congmul  39074  congsub  39077  ntrclsiso  39927  ntrclskb  39929  ntrclsk3  39930  limsupre  41489  0ellimcdiv  41497  limclner  41499  sge0xaddlem2  42284  lincdifsn  43985  itschlc0yqe  44254  itscnhlc0xyqsol  44259