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

Theorem simp11 988
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 979 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  simpl11  1033  simpr11  1042  simp111  1087  simp211  1096  simp311  1105  omeulem1  6828  omeu  6831  ackbij1lem16  8120  coprimeprodsq  13188  pythagtriplem14  13207  pythagtrip  13213  mrelatglb  14615  subglsm  15310  lsmpropd  15314  isfil2  17893  filuni  17922  cxple2a  20595  isosctr  20670  gxdi  21889  measres  24581  bayesth  24702  brbtwn2  25849  colinearalg  25854  ax5seglem3  25875  ofscom  25946  btwndiff  25966  ifscgr  25983  brofs2  26016  brifs2  26017  fscgr  26019  btwnconn1lem1  26026  btwnconn1lem2  26027  btwnconn1lem3  26028  btwnconn1lem4  26029  btwnconn1lem5  26030  btwnconn1lem6  26031  btwnconn1lem7  26032  btwnconn1lem8  26033  btwnconn1lem9  26034  btwnconn1lem10  26035  btwnconn1lem11  26036  btwnconn1lem12  26037  seglecgr12im  26049  seglecgr12  26050  ivthALT  26352  monotuz  27018  congmul  27046  congsub  27049  rpnnen3lem  27116  eqlkr  29971  lkrshp  29977  lshpkrlem5  29986  cvrval3  30284  4noncolr3  30324  4noncolr2  30325  4noncolr1  30326  athgt  30327  3dimlem2  30330  3dimlem3a  30331  3dimlem4a  30334  3dimlem4  30335  3dimlem4OLDN  30336  3dim2  30339  1cvratex  30344  hlatexch4  30352  ps-2b  30353  3atlem1  30354  3atlem2  30355  3atlem4  30357  3atlem5  30358  3atlem6  30359  llnnleat  30384  2atm  30398  ps-2c  30399  llnmlplnN  30410  lplnnlelln  30414  2atmat  30432  2llnjN  30438  lvoli2  30452  lvolnlelln  30455  4atlem3b  30469  4atlem9  30474  4atlem10a  30475  4atlem10  30477  4atlem11a  30478  4atlem11b  30479  4atlem12a  30481  4atlem12b  30482  4at  30484  4at2  30485  lplncvrlvol2  30486  2lplnj  30491  dalemswapyz  30527  dath2  30608  lneq2at  30649  2lnat  30655  cdlema1N  30662  cdlemb  30665  paddasslem15  30705  pmodlem1  30717  llnmod2i2  30734  llnexchb2lem  30739  llnexchb2  30740  dalawlem1  30742  dalawlem3  30744  dalawlem4  30745  dalawlem5  30746  dalawlem6  30747  dalawlem7  30748  dalawlem8  30749  dalawlem9  30750  dalawlem10  30751  dalawlem11  30752  dalawlem12  30753  dalawlem13  30754  dalawlem15  30756  dalaw  30757  osumcllem5N  30831  osumcllem6N  30832  osumcllem7N  30833  osumcllem9N  30835  osumcllem10N  30836  osumcllem11N  30837  pl42lem1N  30850  lhpexle3lem  30882  lhpmcvr5N  30898  lhp2atne  30905  lhp2at0ne  30907  4atexlemswapqr  30934  4atexlemex6  30945  ldilco  30987  ltrneq  31020  trlval2  31034  trlnidat  31044  cdlemd2  31070  cdlemd7  31075  cdlemd8  31076  cdleme7aa  31113  cdleme7c  31116  cdleme7d  31117  cdleme7e  31118  cdleme7ga  31119  cdleme7  31120  cdleme11c  31132  cdleme11e  31134  cdleme11l  31140  cdleme11  31141  cdleme14  31144  cdleme15a  31145  cdleme15c  31147  cdleme16b  31150  cdleme16c  31151  cdleme16d  31152  cdleme16e  31153  cdleme16f  31154  cdleme0nex  31161  cdleme18d  31166  cdleme19b  31175  cdleme19d  31177  cdleme19e  31178  cdleme20f  31185  cdleme20i  31188  cdleme20k  31190  cdleme20l1  31191  cdleme20l2  31192  cdleme20l  31193  cdleme20m  31194  cdleme21a  31196  cdleme21b  31197  cdleme21ct  31200  cdleme21d  31201  cdleme21e  31202  cdleme21f  31203  cdleme21h  31205  cdleme22eALTN  31216  cdleme22f2  31218  cdleme22g  31219  cdleme26e  31230  cdleme26eALTN  31232  cdleme26fALTN  31233  cdleme26f  31234  cdleme26f2ALTN  31235  cdleme26f2  31236  cdleme28a  31241  cdleme28b  31242  cdleme28  31244  cdleme29ex  31245  cdleme29c  31247  cdlemefrs29cpre1  31269  cdlemefr29exN  31273  cdlemefr32sn2aw  31275  cdlemefr29bpre0N  31277  cdlemefr29clN  31278  cdlemefr32fvaN  31280  cdlemefr32fva1  31281  cdlemefs32sn1aw  31285  cdleme43fsv1snlem  31291  cdleme41sn3a  31304  cdleme32fva  31308  cdleme32b  31313  cdleme32d  31315  cdleme32e  31316  cdleme32f  31317  cdleme32le  31318  cdleme35a  31319  cdleme35fnpq  31320  cdleme35b  31321  cdleme35c  31322  cdleme35d  31323  cdleme35e  31324  cdleme35f  31325  cdleme36a  31331  cdleme36m  31332  cdleme37m  31333  cdleme39a  31336  cdleme39n  31337  cdleme40m  31338  cdleme40n  31339  cdleme42e  31350  cdleme42f  31351  cdleme42g  31352  cdleme43bN  31361  cdleme43cN  31362  cdleme43dN  31363  cdleme46f2g2  31364  cdleme46f2g1  31365  cdleme17d2  31366  cdleme48b  31374  cdleme4gfv  31378  cdlemeg49le  31382  cdlemeg46c  31384  cdlemeg46fvaw  31387  cdlemeg46nlpq  31388  cdlemeg46frv  31396  cdlemeg46rgv  31399  cdlemeg46req  31400  cdlemeg46gfre  31403  cdleme50trn1  31420  cdleme50trn2a  31421  cdleme50trn2  31422  cdleme  31431  cdlemf  31434  trlord  31440  cdlemg2ce  31463  cdlemg7fvbwN  31478  cdlemg7aN  31496  cdlemg10bALTN  31507  cdlemg10a  31511  cdlemg10  31512  cdlemg12d  31517  cdlemg12f  31519  cdlemg12g  31520  cdlemg12  31521  cdlemg13a  31522  cdlemg13  31523  cdlemg17b  31533  cdlemg17dN  31534  cdlemg17dALTN  31535  cdlemg17e  31536  cdlemg17f  31537  cdlemg17g  31538  cdlemg17h  31539  cdlemg17i  31540  cdlemg17pq  31543  cdlemg17bq  31544  cdlemg17iqN  31545  cdlemg17  31548  cdlemg18d  31552  cdlemg18  31553  cdlemg19a  31554  cdlemg19  31555  cdlemg21  31557  cdlemg27a  31563  cdlemg28a  31564  cdlemg31b0N  31565  cdlemg27b  31567  cdlemg33b0  31572  cdlemg28b  31574  cdlemg28  31575  cdlemg33a  31577  cdlemg33  31582  cdlemg34  31583  cdlemg35  31584  cdlemg36  31585  ltrnco  31590  trlcone  31599  cdlemg44  31604  cdlemg47  31607  cdlemg48  31608  tendococl  31643  tendoplcl  31652  cdlemh1  31686  cdlemi  31691  cdlemj1  31692  cdlemj2  31693  tendocan  31695  cdlemk6  31708  cdlemki  31712  cdlemksat  31717  cdlemksv2  31718  cdlemk7  31719  cdlemk11  31720  cdlemk12  31721  cdlemkoatnle  31722  cdlemkole  31724  cdlemk14  31725  cdlemk15  31726  cdlemk16a  31727  cdlemk16  31728  cdlemk17  31729  cdlemk1u  31730  cdlemk5u  31732  cdlemk6u  31733  cdlemkuat  31737  cdlemk18  31739  cdlemk19  31740  cdlemk12u  31743  cdlemk21N  31744  cdlemk20  31745  cdlemkoatnle-2N  31746  cdlemk13-2N  31747  cdlemkole-2N  31748  cdlemk14-2N  31749  cdlemk15-2N  31750  cdlemk16-2N  31751  cdlemk17-2N  31752  cdlemk18-2N  31757  cdlemk19-2N  31758  cdlemk7u-2N  31759  cdlemk11u-2N  31760  cdlemk12u-2N  31761  cdlemk21-2N  31762  cdlemk20-2N  31763  cdlemk22  31764  cdlemk23-3  31773  cdlemk25-3  31775  cdlemk26b-3  31776  cdlemk27-3  31778  cdlemk28-3  31779  cdlemk33N  31780  cdlemk37  31785  cdlemky  31797  cdlemk11ta  31800  cdlemkid3N  31804  cdlemk11tc  31816  cdlemk11t  31817  cdlemk45  31818  cdlemk46  31819  cdlemk47  31820  cdlemk48  31821  cdlemk49  31822  cdlemk50  31823  cdlemk51  31824  cdlemk52  31825  cdlemk55b  31831  cdlemkyyN  31833  cdlemk55u1  31836  cdlemk55u  31837  cdlemk39u1  31838  cdlemk39u  31839  cdlemk56  31842  cdleml3N  31849  cdleml4N  31850  cdlemm10N  31990  dihord1  32090  dihord2a  32091  dihord2b  32092  dihord10  32095  dihord11c  32096  dihord2pre  32097  dihord4  32130  dihord5apre  32134  dihmeetlem1N  32162  dihglbcpreN  32172  dihjatc1  32183  dihjatc3  32185  dihmeetlem13N  32191  dihmeetlem20N  32198  baerlem3lem2  32582  baerlem5alem2  32583  baerlem5blem2  32584  hdmap14lem11  32753  hdmap14lem12  32754
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator