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

Theorem simp11 987
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 978 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  simpl11  1032  simpr11  1041  simp111  1086  simp211  1095  simp311  1104  omeulem1  6784  omeu  6787  ackbij1lem16  8071  coprimeprodsq  13138  pythagtriplem14  13157  pythagtrip  13163  mrelatglb  14565  subglsm  15260  lsmpropd  15264  isfil2  17841  filuni  17870  cxple2a  20543  isosctr  20618  gxdi  21837  measres  24529  bayesth  24650  brbtwn2  25748  colinearalg  25753  ax5seglem3  25774  ofscom  25845  btwndiff  25865  ifscgr  25882  brofs2  25915  brifs2  25916  fscgr  25918  btwnconn1lem1  25925  btwnconn1lem2  25926  btwnconn1lem3  25927  btwnconn1lem4  25928  btwnconn1lem5  25929  btwnconn1lem6  25930  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn1lem12  25936  seglecgr12im  25948  seglecgr12  25949  ivthALT  26228  monotuz  26894  congmul  26922  congsub  26925  rpnnen3lem  26992  eqlkr  29582  lkrshp  29588  lshpkrlem5  29597  cvrval3  29895  4noncolr3  29935  4noncolr2  29936  4noncolr1  29937  athgt  29938  3dimlem2  29941  3dimlem3a  29942  3dimlem4a  29945  3dimlem4  29946  3dimlem4OLDN  29947  3dim2  29950  1cvratex  29955  hlatexch4  29963  ps-2b  29964  3atlem1  29965  3atlem2  29966  3atlem4  29968  3atlem5  29969  3atlem6  29970  llnnleat  29995  2atm  30009  ps-2c  30010  llnmlplnN  30021  lplnnlelln  30025  2atmat  30043  2llnjN  30049  lvoli2  30063  lvolnlelln  30066  4atlem3b  30080  4atlem9  30085  4atlem10a  30086  4atlem10  30088  4atlem11a  30089  4atlem11b  30090  4atlem12a  30092  4atlem12b  30093  4at  30095  4at2  30096  lplncvrlvol2  30097  2lplnj  30102  dalemswapyz  30138  dath2  30219  lneq2at  30260  2lnat  30266  cdlema1N  30273  cdlemb  30276  paddasslem15  30316  pmodlem1  30328  llnmod2i2  30345  llnexchb2lem  30350  llnexchb2  30351  dalawlem1  30353  dalawlem3  30355  dalawlem4  30356  dalawlem5  30357  dalawlem6  30358  dalawlem7  30359  dalawlem8  30360  dalawlem9  30361  dalawlem10  30362  dalawlem11  30363  dalawlem12  30364  dalawlem13  30365  dalawlem15  30367  dalaw  30368  osumcllem5N  30442  osumcllem6N  30443  osumcllem7N  30444  osumcllem9N  30446  osumcllem10N  30447  osumcllem11N  30448  pl42lem1N  30461  lhpexle3lem  30493  lhpmcvr5N  30509  lhp2atne  30516  lhp2at0ne  30518  4atexlemswapqr  30545  4atexlemex6  30556  ldilco  30598  ltrneq  30631  trlval2  30645  trlnidat  30655  cdlemd2  30681  cdlemd7  30686  cdlemd8  30687  cdleme7aa  30724  cdleme7c  30727  cdleme7d  30728  cdleme7e  30729  cdleme7ga  30730  cdleme7  30731  cdleme11c  30743  cdleme11e  30745  cdleme11l  30751  cdleme11  30752  cdleme14  30755  cdleme15a  30756  cdleme15c  30758  cdleme16b  30761  cdleme16c  30762  cdleme16d  30763  cdleme16e  30764  cdleme16f  30765  cdleme0nex  30772  cdleme18d  30777  cdleme19b  30786  cdleme19d  30788  cdleme19e  30789  cdleme20f  30796  cdleme20i  30799  cdleme20k  30801  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme20m  30805  cdleme21a  30807  cdleme21b  30808  cdleme21ct  30811  cdleme21d  30812  cdleme21e  30813  cdleme21f  30814  cdleme21h  30816  cdleme22eALTN  30827  cdleme22f2  30829  cdleme22g  30830  cdleme26e  30841  cdleme26eALTN  30843  cdleme26fALTN  30844  cdleme26f  30845  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme28a  30852  cdleme28b  30853  cdleme28  30855  cdleme29ex  30856  cdleme29c  30858  cdlemefrs29cpre1  30880  cdlemefr29exN  30884  cdlemefr32sn2aw  30886  cdlemefr29bpre0N  30888  cdlemefr29clN  30889  cdlemefr32fvaN  30891  cdlemefr32fva1  30892  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdleme41sn3a  30915  cdleme32fva  30919  cdleme32b  30924  cdleme32d  30926  cdleme32e  30927  cdleme32f  30928  cdleme32le  30929  cdleme35a  30930  cdleme35fnpq  30931  cdleme35b  30932  cdleme35c  30933  cdleme35d  30934  cdleme35e  30935  cdleme35f  30936  cdleme36a  30942  cdleme36m  30943  cdleme37m  30944  cdleme39a  30947  cdleme39n  30948  cdleme40m  30949  cdleme40n  30950  cdleme42e  30961  cdleme42f  30962  cdleme42g  30963  cdleme43bN  30972  cdleme43cN  30973  cdleme43dN  30974  cdleme46f2g2  30975  cdleme46f2g1  30976  cdleme17d2  30977  cdleme48b  30985  cdleme4gfv  30989  cdlemeg49le  30993  cdlemeg46c  30995  cdlemeg46fvaw  30998  cdlemeg46nlpq  30999  cdlemeg46frv  31007  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfre  31014  cdleme50trn1  31031  cdleme50trn2a  31032  cdleme50trn2  31033  cdleme  31042  cdlemf  31045  trlord  31051  cdlemg2ce  31074  cdlemg7fvbwN  31089  cdlemg7aN  31107  cdlemg10bALTN  31118  cdlemg10a  31122  cdlemg10  31123  cdlemg12d  31128  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg13  31134  cdlemg17b  31144  cdlemg17dN  31145  cdlemg17dALTN  31146  cdlemg17e  31147  cdlemg17f  31148  cdlemg17g  31149  cdlemg17h  31150  cdlemg17i  31151  cdlemg17pq  31154  cdlemg17bq  31155  cdlemg17iqN  31156  cdlemg17  31159  cdlemg18d  31163  cdlemg18  31164  cdlemg19a  31165  cdlemg19  31166  cdlemg21  31168  cdlemg27a  31174  cdlemg28a  31175  cdlemg31b0N  31176  cdlemg27b  31178  cdlemg33b0  31183  cdlemg28b  31185  cdlemg28  31186  cdlemg33a  31188  cdlemg33  31193  cdlemg34  31194  cdlemg35  31195  cdlemg36  31196  ltrnco  31201  trlcone  31210  cdlemg44  31215  cdlemg47  31218  cdlemg48  31219  tendococl  31254  tendoplcl  31263  cdlemh1  31297  cdlemi  31302  cdlemj1  31303  cdlemj2  31304  tendocan  31306  cdlemk6  31319  cdlemki  31323  cdlemksat  31328  cdlemksv2  31329  cdlemk7  31330  cdlemk11  31331  cdlemk12  31332  cdlemkoatnle  31333  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk16a  31338  cdlemk16  31339  cdlemk17  31340  cdlemk1u  31341  cdlemk5u  31343  cdlemk6u  31344  cdlemkuat  31348  cdlemk18  31350  cdlemk19  31351  cdlemk12u  31354  cdlemk21N  31355  cdlemk20  31356  cdlemkoatnle-2N  31357  cdlemk13-2N  31358  cdlemkole-2N  31359  cdlemk14-2N  31360  cdlemk15-2N  31361  cdlemk16-2N  31362  cdlemk17-2N  31363  cdlemk18-2N  31368  cdlemk19-2N  31369  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk21-2N  31373  cdlemk20-2N  31374  cdlemk22  31375  cdlemk23-3  31384  cdlemk25-3  31386  cdlemk26b-3  31387  cdlemk27-3  31389  cdlemk28-3  31390  cdlemk33N  31391  cdlemk37  31396  cdlemky  31408  cdlemk11ta  31411  cdlemkid3N  31415  cdlemk11tc  31427  cdlemk11t  31428  cdlemk45  31429  cdlemk46  31430  cdlemk47  31431  cdlemk48  31432  cdlemk49  31433  cdlemk50  31434  cdlemk51  31435  cdlemk52  31436  cdlemk55b  31442  cdlemkyyN  31444  cdlemk55u1  31447  cdlemk55u  31448  cdlemk39u1  31449  cdlemk39u  31450  cdlemk56  31453  cdleml3N  31460  cdleml4N  31461  cdlemm10N  31601  dihord1  31701  dihord2a  31702  dihord2b  31703  dihord10  31706  dihord11c  31707  dihord2pre  31708  dihord4  31741  dihord5apre  31745  dihmeetlem1N  31773  dihglbcpreN  31783  dihjatc1  31794  dihjatc3  31796  dihmeetlem13N  31802  dihmeetlem20N  31809  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmap14lem11  32364  hdmap14lem12  32365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator