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

Theorem simp11 1018
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 988 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1009 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  simpl11  1063  simpr11  1072  simp111  1117  simp211  1126  simp311  1135  omeulem1  7019  omeu  7022  ackbij1lem16  8402  coprimeprodsq  13874  pythagtriplem14  13893  pythagtrip  13899  mrelatglb  15352  subglsm  16168  lsmpropd  16172  mdetmul  18427  isfil2  19427  filuni  19456  cxple2a  22142  isosctr  22217  brbtwn2  23149  colinearalg  23154  ax5seglem3  23175  gxdi  23781  measres  26634  bayesth  26820  ofscom  28036  btwndiff  28056  ifscgr  28073  brofs2  28106  brifs2  28107  fscgr  28109  btwnconn1lem1  28116  btwnconn1lem2  28117  btwnconn1lem3  28118  btwnconn1lem4  28119  btwnconn1lem5  28120  btwnconn1lem6  28121  btwnconn1lem7  28122  btwnconn1lem8  28123  btwnconn1lem9  28124  btwnconn1lem10  28125  btwnconn1lem11  28126  btwnconn1lem12  28127  seglecgr12im  28139  seglecgr12  28140  ivthALT  28527  monotuz  29279  congmul  29307  congsub  29310  rpnnen3lem  29377  numclwwlkovf2ex  30676  pmatcollpw1id  30896  lincdifsn  30955  eqlkr  32741  lkrshp  32747  lshpkrlem5  32756  cvrval3  33054  4noncolr3  33094  4noncolr2  33095  4noncolr1  33096  athgt  33097  3dimlem2  33100  3dimlem3a  33101  3dimlem4a  33104  3dimlem4  33105  3dimlem4OLDN  33106  3dim2  33109  1cvratex  33114  hlatexch4  33122  ps-2b  33123  3atlem1  33124  3atlem2  33125  3atlem4  33127  3atlem5  33128  3atlem6  33129  llnnleat  33154  2atm  33168  ps-2c  33169  llnmlplnN  33180  lplnnlelln  33184  2atmat  33202  2llnjN  33208  lvoli2  33222  lvolnlelln  33225  4atlem3b  33239  4atlem9  33244  4atlem10a  33245  4atlem10  33247  4atlem11a  33248  4atlem11b  33249  4atlem12a  33251  4atlem12b  33252  4at  33254  4at2  33255  lplncvrlvol2  33256  2lplnj  33261  dalemswapyz  33297  dath2  33378  lneq2at  33419  2lnat  33425  cdlema1N  33432  cdlemb  33435  paddasslem15  33475  pmodlem1  33487  llnmod2i2  33504  llnexchb2lem  33509  llnexchb2  33510  dalawlem1  33512  dalawlem3  33514  dalawlem4  33515  dalawlem5  33516  dalawlem6  33517  dalawlem7  33518  dalawlem8  33519  dalawlem9  33520  dalawlem10  33521  dalawlem11  33522  dalawlem12  33523  dalawlem13  33524  dalawlem15  33526  dalaw  33527  osumcllem5N  33601  osumcllem6N  33602  osumcllem7N  33603  osumcllem9N  33605  osumcllem10N  33606  osumcllem11N  33607  pl42lem1N  33620  lhpexle3lem  33652  lhpmcvr5N  33668  lhp2atne  33675  lhp2at0ne  33677  4atexlemswapqr  33704  4atexlemex6  33715  ldilco  33757  ltrneq  33790  trlval2  33804  trlnidat  33814  cdlemd2  33840  cdlemd7  33845  cdlemd8  33846  cdleme7aa  33883  cdleme7c  33886  cdleme7d  33887  cdleme7e  33888  cdleme7ga  33889  cdleme7  33890  cdleme11c  33902  cdleme11e  33904  cdleme11l  33910  cdleme11  33911  cdleme14  33914  cdleme15a  33915  cdleme15c  33917  cdleme16b  33920  cdleme16c  33921  cdleme16d  33922  cdleme16e  33923  cdleme16f  33924  cdleme0nex  33931  cdleme18d  33936  cdleme19b  33945  cdleme19d  33947  cdleme19e  33948  cdleme20f  33955  cdleme20i  33958  cdleme20k  33960  cdleme20l1  33961  cdleme20l2  33962  cdleme20l  33963  cdleme20m  33964  cdleme21a  33966  cdleme21b  33967  cdleme21ct  33970  cdleme21d  33971  cdleme21e  33972  cdleme21f  33973  cdleme21h  33975  cdleme22eALTN  33986  cdleme22f2  33988  cdleme22g  33989  cdleme26e  34000  cdleme26eALTN  34002  cdleme26fALTN  34003  cdleme26f  34004  cdleme26f2ALTN  34005  cdleme26f2  34006  cdleme28a  34011  cdleme28b  34012  cdleme28  34014  cdleme29ex  34015  cdleme29c  34017  cdlemefrs29cpre1  34039  cdlemefr29exN  34043  cdlemefr32sn2aw  34045  cdlemefr29bpre0N  34047  cdlemefr29clN  34048  cdlemefr32fvaN  34050  cdlemefr32fva1  34051  cdlemefs32sn1aw  34055  cdleme43fsv1snlem  34061  cdleme41sn3a  34074  cdleme32fva  34078  cdleme32b  34083  cdleme32d  34085  cdleme32e  34086  cdleme32f  34087  cdleme32le  34088  cdleme35a  34089  cdleme35fnpq  34090  cdleme35b  34091  cdleme35c  34092  cdleme35d  34093  cdleme35e  34094  cdleme35f  34095  cdleme36a  34101  cdleme36m  34102  cdleme37m  34103  cdleme39a  34106  cdleme39n  34107  cdleme40m  34108  cdleme40n  34109  cdleme42e  34120  cdleme42f  34121  cdleme42g  34122  cdleme43bN  34131  cdleme43cN  34132  cdleme43dN  34133  cdleme46f2g2  34134  cdleme46f2g1  34135  cdleme17d2  34136  cdleme48b  34144  cdleme4gfv  34148  cdlemeg49le  34152  cdlemeg46c  34154  cdlemeg46fvaw  34157  cdlemeg46nlpq  34158  cdlemeg46frv  34166  cdlemeg46rgv  34169  cdlemeg46req  34170  cdlemeg46gfre  34173  cdleme50trn1  34190  cdleme50trn2a  34191  cdleme50trn2  34192  cdleme  34201  cdlemf  34204  trlord  34210  cdlemg2ce  34233  cdlemg7fvbwN  34248  cdlemg7aN  34266  cdlemg10bALTN  34277  cdlemg10a  34281  cdlemg10  34282  cdlemg12d  34287  cdlemg12f  34289  cdlemg12g  34290  cdlemg12  34291  cdlemg13a  34292  cdlemg13  34293  cdlemg17b  34303  cdlemg17dN  34304  cdlemg17dALTN  34305  cdlemg17e  34306  cdlemg17f  34307  cdlemg17g  34308  cdlemg17h  34309  cdlemg17i  34310  cdlemg17pq  34313  cdlemg17bq  34314  cdlemg17iqN  34315  cdlemg17  34318  cdlemg18d  34322  cdlemg18  34323  cdlemg19a  34324  cdlemg19  34325  cdlemg21  34327  cdlemg27a  34333  cdlemg28a  34334  cdlemg31b0N  34335  cdlemg27b  34337  cdlemg33b0  34342  cdlemg28b  34344  cdlemg28  34345  cdlemg33a  34347  cdlemg33  34352  cdlemg34  34353  cdlemg35  34354  cdlemg36  34355  ltrnco  34360  trlcone  34369  cdlemg44  34374  cdlemg47  34377  cdlemg48  34378  tendococl  34413  tendoplcl  34422  cdlemh1  34456  cdlemi  34461  cdlemj1  34462  cdlemj2  34463  tendocan  34465  cdlemk6  34478  cdlemki  34482  cdlemksat  34487  cdlemksv2  34488  cdlemk7  34489  cdlemk11  34490  cdlemk12  34491  cdlemkoatnle  34492  cdlemkole  34494  cdlemk14  34495  cdlemk15  34496  cdlemk16a  34497  cdlemk16  34498  cdlemk17  34499  cdlemk1u  34500  cdlemk5u  34502  cdlemk6u  34503  cdlemkuat  34507  cdlemk18  34509  cdlemk19  34510  cdlemk12u  34513  cdlemk21N  34514  cdlemk20  34515  cdlemkoatnle-2N  34516  cdlemk13-2N  34517  cdlemkole-2N  34518  cdlemk14-2N  34519  cdlemk15-2N  34520  cdlemk16-2N  34521  cdlemk17-2N  34522  cdlemk18-2N  34527  cdlemk19-2N  34528  cdlemk7u-2N  34529  cdlemk11u-2N  34530  cdlemk12u-2N  34531  cdlemk21-2N  34532  cdlemk20-2N  34533  cdlemk22  34534  cdlemk23-3  34543  cdlemk25-3  34545  cdlemk26b-3  34546  cdlemk27-3  34548  cdlemk28-3  34549  cdlemk33N  34550  cdlemk37  34555  cdlemky  34567  cdlemk11ta  34570  cdlemkid3N  34574  cdlemk11tc  34586  cdlemk11t  34587  cdlemk45  34588  cdlemk46  34589  cdlemk47  34590  cdlemk48  34591  cdlemk49  34592  cdlemk50  34593  cdlemk51  34594  cdlemk52  34595  cdlemk55b  34601  cdlemkyyN  34603  cdlemk55u1  34606  cdlemk55u  34607  cdlemk39u1  34608  cdlemk39u  34609  cdlemk56  34612  cdleml3N  34619  cdleml4N  34620  cdlemm10N  34760  dihord1  34860  dihord2a  34861  dihord2b  34862  dihord10  34865  dihord11c  34866  dihord2pre  34867  dihord4  34900  dihord5apre  34904  dihmeetlem1N  34932  dihglbcpreN  34942  dihjatc1  34953  dihjatc3  34955  dihmeetlem13N  34961  dihmeetlem20N  34968  baerlem3lem2  35352  baerlem5alem2  35353  baerlem5blem2  35354  hdmap14lem11  35523  hdmap14lem12  35524
  Copyright terms: Public domain W3C validator