Theorem simp12 1092

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

Assertion

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

Proof of Theorem simp12

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

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:  simpl12  1137  simpr12  1146  simp112  1191  simp212  1200  simp312  1209  dvdsgcd  15261  coprimeprodsq  15513  pythagtriplem4  15524  pythagtriplem13  15532  pythagtriplem14  15533  pythagtriplem16  15535  pythagtrip  15539  pceu  15551  mremre  16264  lsmpropd  18090  m2cpminvid  20558  decpmatid  20575  mply1topmatcllem  20608  cmpsublem  21202  isfil2  21660  cxple2a  24445  isosctr  24551  brbtwn2  25785  colinearalg  25790  ax5seg  25818  axcontlem4  25847  bayesth  30501  bnj1204  31080  bnj1279  31086  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  btwnconn1lem12  32205  seglecgr12im  32217  seglecgr12  32218  ivthALT  32330  islshpcv  34340  lkrshp  34392  lshpsmreu  34396  lshpkrlem5  34401  cvrval3  34699  4noncolr3  34739  4noncolr2  34740  4noncolr1  34741  athgt  34742  3dimlem2  34745  3dimlem3a  34746  3dimlem4a  34749  3dimlem4  34750  3dimlem4OLDN  34751  1cvratex  34759  hlatexch4  34767  ps-2b  34768  3atlem4  34772  llnnleat  34799  2atm  34813  ps-2c  34814  llnmlplnN  34825  lplnnlelln  34829  2atmat  34847  lvoli2  34867  lvolnlelln  34870  4atlem3b  34884  4atlem10  34892  4atlem11a  34893  4atlem11b  34894  4atlem12a  34896  lplncvrlvol2  34901  2lplnja  34905  dalemswapyz  34942  lneq2at  35064  2lnat  35070  cdlema1N  35077  cdlemb  35080  paddasslem15  35120  pmodlem1  35132  llnmod2i2  35149  llnexchb2lem  35154  dalawlem1  35157  dalawlem3  35159  dalawlem4  35160  dalawlem6  35162  dalawlem7  35163  dalawlem9  35165  dalawlem10  35166  dalawlem11  35167  dalawlem12  35168  dalawlem13  35169  dalawlem15  35171  osumcllem5N  35246  osumcllem6N  35247  osumcllem7N  35248  osumcllem9N  35250  osumcllem10N  35251  osumcllem11N  35252  pl42lem1N  35265  lhpmcvr5N  35313  lhp2atne  35320  lhp2at0ne  35322  4atexlempw  35335  4atexlemex6  35360  4atexlem7  35361  ldilco  35402  ltrneq  35435  trlval2  35450  trlnidat  35460  cdlemd7  35491  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  cdleme20k  35607  cdleme20l1  35608  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme21a  35613  cdleme21b  35614  cdleme21ct  35617  cdleme21d  35618  cdleme21e  35619  cdleme21f  35620  cdleme21h  35622  cdleme21i  35623  cdleme22eALTN  35633  cdleme22f2  35635  cdleme22g  35636  cdleme24  35640  cdleme25a  35641  cdleme25c  35643  cdleme25dN  35644  cdleme26e  35647  cdleme26ee  35648  cdleme26eALTN  35649  cdleme27N  35657  cdleme28a  35658  cdleme28b  35659  cdleme28  35661  cdlemefr32sn2aw  35692  cdlemefs32sn1aw  35702  cdleme43fsv1snlem  35708  cdleme41sn3a  35721  cdleme32c  35731  cdleme32e  35733  cdleme32le  35735  cdleme35a  35736  cdleme35b  35738  cdleme35c  35739  cdleme35e  35741  cdleme35f  35742  cdleme36a  35748  cdleme36m  35749  cdleme39a  35753  cdleme40m  35755  cdleme40n  35756  cdleme43bN  35778  cdleme43dN  35780  cdleme46f2g2  35781  cdleme46f2g1  35782  cdleme17d2  35783  cdleme4gfv  35795  cdlemeg49le  35799  cdlemeg46c  35801  cdlemeg46fvaw  35804  cdlemeg46nlpq  35805  cdlemeg46gfre  35820  cdleme50trn2  35839  cdleme  35848  cdlemg2idN  35884  cdlemg7fvbwN  35895  cdlemg10bALTN  35924  cdlemg10a  35928  cdlemg12d  35934  cdlemg12g  35937  cdlemg12  35938  cdlemg13a  35939  cdlemg13  35940  cdlemg17b  35950  cdlemg17dN  35951  cdlemg17dALTN  35952  cdlemg17e  35953  cdlemg17f  35954  cdlemg17i  35957  cdlemg17pq  35960  cdlemg17bq  35961  cdlemg17iqN  35962  cdlemg18d  35969  cdlemg18  35970  cdlemg19a  35971  cdlemg19  35972  cdlemg21  35974  cdlemg27a  35980  cdlemg28a  35981  cdlemg31b0N  35982  cdlemg27b  35984  cdlemg31c  35987  cdlemg33b0  35989  cdlemg33c0  35990  cdlemg28  35992  cdlemg33a  35994  cdlemg33  35999  cdlemg36  36002  ltrnco  36007  cdlemg44  36021  cdlemg47  36024  tendococl  36060  tendoplcl  36069  cdlemh1  36103  cdlemh2  36104  cdlemh  36105  cdlemi  36108  tendocan  36112  cdlemk5  36124  cdlemk6  36125  cdlemk7  36136  cdlemk11  36137  cdlemk12  36138  cdlemkole  36141  cdlemk14  36142  cdlemk15  36143  cdlemk16a  36144  cdlemk16  36145  cdlemk18  36156  cdlemk19  36157  cdlemk7u  36158  cdlemk11u  36159  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  cdlemk27-3  36195  cdlemk33N  36197  cdlemk11ta  36217  cdlemkid3N  36221  cdlemk11tc  36233  cdlemk11t  36234  cdlemk45  36235  cdlemk46  36236  cdlemk47  36237  cdlemk48  36238  cdlemk49  36239  cdlemk50  36240  cdlemk51  36241  cdlemk52  36242  cdlemk53a  36243  cdlemk55b  36248  cdlemkyyN  36250  cdlemk55u1  36253  cdlemk39u1  36255  cdlemk56  36259  cdlemm10N  36407  dihord1  36507  dihord2a  36508  dihord2b  36509  dihord10  36512  dihord4  36547  dihord5apre  36551  dihglblem2N  36583  dihjatc1  36600  dihjatc2N  36601  dihjatc3  36602  dihmeetlem15N  36610  dihmeetlem20N  36615  mapdpglem24  36993  hdmap14lem11  37170  hdmap14lem12  37171  mzpsubst  37311  monotuz  37506  congmul  37534  congsub  37537  ntrclsiso  38365  ntrclskb  38367  ntrclsk3  38368  infleinf  39588  mullimc  39848  mullimcf  39855  0ellimcdiv  39881  limclner  39883  sge0xaddlem2  40651  lincdifsn  42213