MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp11 Structured version   Unicode version

Theorem simp11 1027
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
StepHypRef Expression
1 simp1 997 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1018 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 185  df-an 371  df-3an 976
This theorem is referenced by:  simpl11  1072  simpr11  1081  simp111  1126  simp211  1135  simp311  1144  omeulem1  7233  omeu  7236  ackbij1lem16  8618  coprimeprodsq  14314  pythagtriplem14  14333  pythagtrip  14339  mrelatglb  15792  subglsm  16669  lsmpropd  16673  mdetmul  19102  decpmatid  19248  isfil2  20334  filuni  20363  cxple2a  23056  isosctr  23131  brbtwn2  24184  colinearalg  24189  ax5seglem3  24210  numclwwlkovf2ex  25062  gxdi  25274  measres  28170  bayesth  28355  ofscom  29632  btwndiff  29652  ifscgr  29669  brofs2  29702  brifs2  29703  fscgr  29705  btwnconn1lem1  29712  btwnconn1lem2  29713  btwnconn1lem3  29714  btwnconn1lem4  29715  btwnconn1lem5  29716  btwnconn1lem6  29717  btwnconn1lem7  29718  btwnconn1lem8  29719  btwnconn1lem9  29720  btwnconn1lem10  29721  btwnconn1lem11  29722  btwnconn1lem12  29723  seglecgr12im  29735  seglecgr12  29736  ivthALT  30128  monotuz  30852  congmul  30880  congsub  30883  rpnnen3lem  30948  lincdifsn  32760  eqlkr  34564  lkrshp  34570  lshpkrlem5  34579  cvrval3  34877  4noncolr3  34917  4noncolr2  34918  4noncolr1  34919  athgt  34920  3dimlem2  34923  3dimlem3a  34924  3dimlem4a  34927  3dimlem4  34928  3dimlem4OLDN  34929  3dim2  34932  1cvratex  34937  hlatexch4  34945  ps-2b  34946  3atlem1  34947  3atlem2  34948  3atlem4  34950  3atlem5  34951  3atlem6  34952  llnnleat  34977  2atm  34991  ps-2c  34992  llnmlplnN  35003  lplnnlelln  35007  2atmat  35025  2llnjN  35031  lvoli2  35045  lvolnlelln  35048  4atlem3b  35062  4atlem9  35067  4atlem10a  35068  4atlem10  35070  4atlem11a  35071  4atlem11b  35072  4atlem12a  35074  4atlem12b  35075  4at  35077  4at2  35078  lplncvrlvol2  35079  2lplnj  35084  dalemswapyz  35120  dath2  35201  lneq2at  35242  2lnat  35248  cdlema1N  35255  cdlemb  35258  paddasslem15  35298  pmodlem1  35310  llnmod2i2  35327  llnexchb2lem  35332  llnexchb2  35333  dalawlem1  35335  dalawlem3  35337  dalawlem4  35338  dalawlem5  35339  dalawlem6  35340  dalawlem7  35341  dalawlem8  35342  dalawlem9  35343  dalawlem10  35344  dalawlem11  35345  dalawlem12  35346  dalawlem13  35347  dalawlem15  35349  dalaw  35350  osumcllem5N  35424  osumcllem6N  35425  osumcllem7N  35426  osumcllem9N  35428  osumcllem10N  35429  osumcllem11N  35430  pl42lem1N  35443  lhpexle3lem  35475  lhpmcvr5N  35491  lhp2atne  35498  lhp2at0ne  35500  4atexlemswapqr  35527  4atexlemex6  35538  ldilco  35580  ltrneq  35613  trlval2  35628  trlnidat  35638  cdlemd2  35664  cdlemd7  35669  cdlemd8  35670  cdleme7aa  35707  cdleme7c  35710  cdleme7d  35711  cdleme7e  35712  cdleme7ga  35713  cdleme7  35714  cdleme11c  35726  cdleme11e  35728  cdleme11l  35734  cdleme11  35735  cdleme14  35738  cdleme15a  35739  cdleme15c  35741  cdleme16b  35744  cdleme16c  35745  cdleme16d  35746  cdleme16e  35747  cdleme16f  35748  cdleme0nex  35755  cdleme18d  35760  cdleme19b  35770  cdleme19d  35772  cdleme19e  35773  cdleme20f  35780  cdleme20i  35783  cdleme20k  35785  cdleme20l1  35786  cdleme20l2  35787  cdleme20l  35788  cdleme20m  35789  cdleme21a  35791  cdleme21b  35792  cdleme21ct  35795  cdleme21d  35796  cdleme21e  35797  cdleme21f  35798  cdleme21h  35800  cdleme22eALTN  35811  cdleme22f2  35813  cdleme22g  35814  cdleme26e  35825  cdleme26eALTN  35827  cdleme26fALTN  35828  cdleme26f  35829  cdleme26f2ALTN  35830  cdleme26f2  35831  cdleme28a  35836  cdleme28b  35837  cdleme28  35839  cdleme29ex  35840  cdleme29c  35842  cdlemefrs29cpre1  35864  cdlemefr29exN  35868  cdlemefr32sn2aw  35870  cdlemefr29bpre0N  35872  cdlemefr29clN  35873  cdlemefr32fvaN  35875  cdlemefr32fva1  35876  cdlemefs32sn1aw  35880  cdleme43fsv1snlem  35886  cdleme41sn3a  35899  cdleme32fva  35903  cdleme32b  35908  cdleme32d  35910  cdleme32e  35911  cdleme32f  35912  cdleme32le  35913  cdleme35a  35914  cdleme35fnpq  35915  cdleme35b  35916  cdleme35c  35917  cdleme35d  35918  cdleme35e  35919  cdleme35f  35920  cdleme36a  35926  cdleme36m  35927  cdleme37m  35928  cdleme39a  35931  cdleme39n  35932  cdleme40m  35933  cdleme40n  35934  cdleme42e  35945  cdleme42f  35946  cdleme42g  35947  cdleme43bN  35956  cdleme43cN  35957  cdleme43dN  35958  cdleme46f2g2  35959  cdleme46f2g1  35960  cdleme17d2  35961  cdleme48b  35969  cdleme4gfv  35973  cdlemeg49le  35977  cdlemeg46c  35979  cdlemeg46fvaw  35982  cdlemeg46nlpq  35983  cdlemeg46frv  35991  cdlemeg46rgv  35994  cdlemeg46req  35995  cdlemeg46gfre  35998  cdleme50trn1  36015  cdleme50trn2a  36016  cdleme50trn2  36017  cdleme  36026  cdlemf  36029  trlord  36035  cdlemg2ce  36058  cdlemg7fvbwN  36073  cdlemg7aN  36091  cdlemg10bALTN  36102  cdlemg10a  36106  cdlemg10  36107  cdlemg12d  36112  cdlemg12f  36114  cdlemg12g  36115  cdlemg12  36116  cdlemg13a  36117  cdlemg13  36118  cdlemg17b  36128  cdlemg17dN  36129  cdlemg17dALTN  36130  cdlemg17e  36131  cdlemg17f  36132  cdlemg17g  36133  cdlemg17h  36134  cdlemg17i  36135  cdlemg17pq  36138  cdlemg17bq  36139  cdlemg17iqN  36140  cdlemg17  36143  cdlemg18d  36147  cdlemg18  36148  cdlemg19a  36149  cdlemg19  36150  cdlemg21  36152  cdlemg27a  36158  cdlemg28a  36159  cdlemg31b0N  36160  cdlemg27b  36162  cdlemg33b0  36167  cdlemg28b  36169  cdlemg28  36170  cdlemg33a  36172  cdlemg33  36177  cdlemg34  36178  cdlemg35  36179  cdlemg36  36180  ltrnco  36185  trlcone  36194  cdlemg44  36199  cdlemg47  36202  cdlemg48  36203  tendococl  36238  tendoplcl  36247  cdlemh1  36281  cdlemi  36286  cdlemj1  36287  cdlemj2  36288  tendocan  36290  cdlemk6  36303  cdlemki  36307  cdlemksat  36312  cdlemksv2  36313  cdlemk7  36314  cdlemk11  36315  cdlemk12  36316  cdlemkoatnle  36317  cdlemkole  36319  cdlemk14  36320  cdlemk15  36321  cdlemk16a  36322  cdlemk16  36323  cdlemk17  36324  cdlemk1u  36325  cdlemk5u  36327  cdlemk6u  36328  cdlemkuat  36332  cdlemk18  36334  cdlemk19  36335  cdlemk12u  36338  cdlemk21N  36339  cdlemk20  36340  cdlemkoatnle-2N  36341  cdlemk13-2N  36342  cdlemkole-2N  36343  cdlemk14-2N  36344  cdlemk15-2N  36345  cdlemk16-2N  36346  cdlemk17-2N  36347  cdlemk18-2N  36352  cdlemk19-2N  36353  cdlemk7u-2N  36354  cdlemk11u-2N  36355  cdlemk12u-2N  36356  cdlemk21-2N  36357  cdlemk20-2N  36358  cdlemk22  36359  cdlemk23-3  36368  cdlemk25-3  36370  cdlemk26b-3  36371  cdlemk27-3  36373  cdlemk28-3  36374  cdlemk33N  36375  cdlemk37  36380  cdlemky  36392  cdlemk11ta  36395  cdlemkid3N  36399  cdlemk11tc  36411  cdlemk11t  36412  cdlemk45  36413  cdlemk46  36414  cdlemk47  36415  cdlemk48  36416  cdlemk49  36417  cdlemk50  36418  cdlemk51  36419  cdlemk52  36420  cdlemk55b  36426  cdlemkyyN  36428  cdlemk55u1  36431  cdlemk55u  36432  cdlemk39u1  36433  cdlemk39u  36434  cdlemk56  36437  cdleml3N  36444  cdleml4N  36445  cdlemm10N  36585  dihord1  36685  dihord2a  36686  dihord2b  36687  dihord10  36690  dihord11c  36691  dihord2pre  36692  dihord4  36725  dihord5apre  36729  dihmeetlem1N  36757  dihglbcpreN  36767  dihjatc1  36778  dihjatc3  36780  dihmeetlem13N  36786  dihmeetlem20N  36793  baerlem3lem2  37177  baerlem5alem2  37178  baerlem5blem2  37179  hdmap14lem11  37348  hdmap14lem12  37349
  Copyright terms: Public domain W3C validator