Theorem simp11 1091

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

Assertion

Ref	Expression
simp11	|- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )

Proof of Theorem simp11

Step	Hyp	Ref	Expression
1		simp1 1061	. 2 |- ( ( ph /\ ps /\ ch ) -> ph )
2	1	3ad2ant1 1082	1 |- ( ( ( ph /\ ps /\ ch ) /\ th /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  simpl11  1136  simpr11  1145  simp111  1190  simp211  1199  simp311  1208  funcnvqpOLD  5953  omeulem1  7662  omeu  7665  ackbij1lem16  9057  coprimeprodsq  15513  pythagtriplem14  15533  pythagtrip  15539  mrelatglb  17184  subglsm  18086  lsmpropd  18090  mdetmul  20429  decpmatid  20575  isfil2  21660  filuni  21689  cxple2a  24445  isosctr  24551  brbtwn2  25785  colinearalg  25790  ax5seglem3  25811  numclwwlkovf2ex  27219  measres  30285  bayesth  30501  nolesgn2o  31824  nolesgn2ores  31825  nolt02o  31845  ofscom  32114  btwndiff  32134  ifscgr  32151  brofs2  32184  brifs2  32185  fscgr  32187  btwnconn1lem1  32194  btwnconn1lem2  32195  btwnconn1lem3  32196  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem7  32200  btwnconn1lem8  32201  btwnconn1lem9  32202  btwnconn1lem10  32203  btwnconn1lem11  32204  btwnconn1lem12  32205  seglecgr12im  32217  seglecgr12  32218  ivthALT  32330  eqlkr  34386  lkrshp  34392  lshpkrlem5  34401  cvrval3  34699  4noncolr3  34739  4noncolr2  34740  4noncolr1  34741  athgt  34742  3dimlem2  34745  3dimlem3a  34746  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  3dim2  34754  1cvratex  34759  hlatexch4  34767  ps-2b  34768  3atlem1  34769  3atlem2  34770  3atlem4  34772  3atlem5  34773  3atlem6  34774  llnnleat  34799  2atm  34813  ps-2c  34814  llnmlplnN  34825  lplnnlelln  34829  2atmat  34847  2llnjN  34853  lvoli2  34867  lvolnlelln  34870  4atlem3b  34884  4atlem9  34889  4atlem10a  34890  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem12a  34896  4atlem12b  34897  4at  34899  4at2  34900  lplncvrlvol2  34901  2lplnj  34906  dalemswapyz  34942  dath2  35023  lneq2at  35064  2lnat  35070  cdlema1N  35077  cdlemb  35080  paddasslem15  35120  pmodlem1  35132  llnmod2i2  35149  llnexchb2lem  35154  llnexchb2  35155  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem5  35161  dalawlem6  35162  dalawlem7  35163  dalawlem8  35164  dalawlem9  35165  dalawlem10  35166  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  dalawlem15  35171  dalaw  35172  osumcllem5N  35246  osumcllem6N  35247  osumcllem7N  35248  osumcllem9N  35250  osumcllem10N  35251  osumcllem11N  35252  pl42lem1N  35265  lhpexle3lem  35297  lhpmcvr5N  35313  lhp2atne  35320  lhp2at0ne  35322  4atexlemswapqr  35349  4atexlemex6  35360  ldilco  35402  ltrneq  35435  trlval2  35450  trlnidat  35460  cdlemd2  35486  cdlemd7  35491  cdlemd8  35492  cdleme7aa  35529  cdleme7c  35532  cdleme7d  35533  cdleme7e  35534  cdleme7ga  35535  cdleme7  35536  cdleme11c  35548  cdleme11e  35550  cdleme11l  35556  cdleme11  35557  cdleme14  35560  cdleme15a  35561  cdleme15c  35563  cdleme16b  35566  cdleme16c  35567  cdleme16d  35568  cdleme16e  35569  cdleme16f  35570  cdleme0nex  35577  cdleme18d  35582  cdleme19b  35592  cdleme19d  35594  cdleme19e  35595  cdleme20f  35602  cdleme20i  35605  cdleme20k  35607  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21a  35613  cdleme21b  35614  cdleme21ct  35617  cdleme21d  35618  cdleme21e  35619  cdleme21f  35620  cdleme21h  35622  cdleme22eALTN  35633  cdleme22f2  35635  cdleme22g  35636  cdleme26e  35647  cdleme26eALTN  35649  cdleme26fALTN  35650  cdleme26f  35651  cdleme26f2ALTN  35652  cdleme26f2  35653  cdleme28a  35658  cdleme28b  35659  cdleme28  35661  cdleme29ex  35662  cdleme29c  35664  cdlemefrs29cpre1  35686  cdlemefr29exN  35690  cdlemefr32sn2aw  35692  cdlemefr29bpre0N  35694  cdlemefr29clN  35695  cdlemefr32fvaN  35697  cdlemefr32fva1  35698  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32fva  35725  cdleme32b  35730  cdleme32d  35732  cdleme32e  35733  cdleme32f  35734  cdleme32le  35735  cdleme35a  35736  cdleme35fnpq  35737  cdleme35b  35738  cdleme35c  35739  cdleme35d  35740  cdleme35e  35741  cdleme35f  35742  cdleme36a  35748  cdleme36m  35749  cdleme37m  35750  cdleme39a  35753  cdleme39n  35754  cdleme40m  35755  cdleme40n  35756  cdleme42e  35767  cdleme42f  35768  cdleme42g  35769  cdleme43bN  35778  cdleme43cN  35779  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme17d2  35783  cdleme48b  35791  cdleme4gfv  35795  cdlemeg49le  35799  cdlemeg46c  35801  cdlemeg46fvaw  35804  cdlemeg46nlpq  35805  cdlemeg46frv  35813  cdlemeg46rgv  35816  cdlemeg46req  35817  cdlemeg46gfre  35820  cdleme50trn1  35837  cdleme50trn2a  35838  cdleme50trn2  35839  cdleme  35848  cdlemf  35851  trlord  35857  cdlemg2ce  35880  cdlemg7fvbwN  35895  cdlemg7aN  35913  cdlemg10bALTN  35924  cdlemg10a  35928  cdlemg10  35929  cdlemg12d  35934  cdlemg12f  35936  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17f  35954  cdlemg17g  35955  cdlemg17h  35956  cdlemg17i  35957  cdlemg17pq  35960  cdlemg17bq  35961  cdlemg17iqN  35962  cdlemg17  35965  cdlemg18d  35969  cdlemg18  35970  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg28a  35981  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg33b0  35989  cdlemg28b  35991  cdlemg28  35992  cdlemg33a  35994  cdlemg33  35999  cdlemg34  36000  cdlemg35  36001  cdlemg36  36002  ltrnco  36007  trlcone  36016  cdlemg44  36021  cdlemg47  36024  cdlemg48  36025  tendococl  36060  tendoplcl  36069  cdlemh1  36103  cdlemi  36108  cdlemj1  36109  cdlemj2  36110  tendocan  36112  cdlemk6  36125  cdlemki  36129  cdlemksat  36134  cdlemksv2  36135  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkoatnle  36139  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk17  36146  cdlemk1u  36147  cdlemk5u  36149  cdlemk6u  36150  cdlemkuat  36154  cdlemk18  36156  cdlemk19  36157  cdlemk12u  36160  cdlemk21N  36161  cdlemk20  36162  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk21-2N  36179  cdlemk20-2N  36180  cdlemk22  36181  cdlemk23-3  36190  cdlemk25-3  36192  cdlemk26b-3  36193  cdlemk27-3  36195  cdlemk28-3  36196  cdlemk33N  36197  cdlemk37  36202  cdlemky  36214  cdlemk11ta  36217  cdlemkid3N  36221  cdlemk11tc  36233  cdlemk11t  36234  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk55b  36248  cdlemkyyN  36250  cdlemk55u1  36253  cdlemk55u  36254  cdlemk39u1  36255  cdlemk39u  36256  cdlemk56  36259  cdleml3N  36266  cdleml4N  36267  cdlemm10N  36407  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord10  36512  dihord11c  36513  dihord2pre  36514  dihord4  36547  dihord5apre  36551  dihmeetlem1N  36579  dihglbcpreN  36589  dihjatc1  36600  dihjatc3  36602  dihmeetlem13N  36608  dihmeetlem20N  36615  baerlem3lem2  36999  baerlem5alem2  37000  baerlem5blem2  37001  hdmap14lem11  37170  hdmap14lem12  37171  monotuz  37506  congmul  37534  congsub  37537  rpnnen3lem  37598  ntrclsiso  38365  ntrclskb  38367  ntrclsk3  38368  wessf1ornlem  39371  infleinf  39588  lincdifsn  42213