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

Theorem simp11 1021
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 991 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
213ad2ant1 1012 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  simpl11  1066  simpr11  1075  simp111  1120  simp211  1129  simp311  1138  omeulem1  7221  omeu  7224  ackbij1lem16  8604  coprimeprodsq  14181  pythagtriplem14  14200  pythagtrip  14206  mrelatglb  15660  subglsm  16480  lsmpropd  16484  mdetmul  18885  decpmatid  19031  isfil2  20085  filuni  20114  cxple2a  22801  isosctr  22876  brbtwn2  23877  colinearalg  23882  ax5seglem3  23903  numclwwlkovf2ex  24749  gxdi  24960  measres  27819  bayesth  28004  ofscom  29220  btwndiff  29240  ifscgr  29257  brofs2  29290  brifs2  29291  fscgr  29293  btwnconn1lem1  29300  btwnconn1lem2  29301  btwnconn1lem3  29302  btwnconn1lem4  29303  btwnconn1lem5  29304  btwnconn1lem6  29305  btwnconn1lem7  29306  btwnconn1lem8  29307  btwnconn1lem9  29308  btwnconn1lem10  29309  btwnconn1lem11  29310  btwnconn1lem12  29311  seglecgr12im  29323  seglecgr12  29324  ivthALT  29717  monotuz  30468  congmul  30496  congsub  30499  rpnnen3lem  30566  lincdifsn  31973  eqlkr  33771  lkrshp  33777  lshpkrlem5  33786  cvrval3  34084  4noncolr3  34124  4noncolr2  34125  4noncolr1  34126  athgt  34127  3dimlem2  34130  3dimlem3a  34131  3dimlem4a  34134  3dimlem4  34135  3dimlem4OLDN  34136  3dim2  34139  1cvratex  34144  hlatexch4  34152  ps-2b  34153  3atlem1  34154  3atlem2  34155  3atlem4  34157  3atlem5  34158  3atlem6  34159  llnnleat  34184  2atm  34198  ps-2c  34199  llnmlplnN  34210  lplnnlelln  34214  2atmat  34232  2llnjN  34238  lvoli2  34252  lvolnlelln  34255  4atlem3b  34269  4atlem9  34274  4atlem10a  34275  4atlem10  34277  4atlem11a  34278  4atlem11b  34279  4atlem12a  34281  4atlem12b  34282  4at  34284  4at2  34285  lplncvrlvol2  34286  2lplnj  34291  dalemswapyz  34327  dath2  34408  lneq2at  34449  2lnat  34455  cdlema1N  34462  cdlemb  34465  paddasslem15  34505  pmodlem1  34517  llnmod2i2  34534  llnexchb2lem  34539  llnexchb2  34540  dalawlem1  34542  dalawlem3  34544  dalawlem4  34545  dalawlem5  34546  dalawlem6  34547  dalawlem7  34548  dalawlem8  34549  dalawlem9  34550  dalawlem10  34551  dalawlem11  34552  dalawlem12  34553  dalawlem13  34554  dalawlem15  34556  dalaw  34557  osumcllem5N  34631  osumcllem6N  34632  osumcllem7N  34633  osumcllem9N  34635  osumcllem10N  34636  osumcllem11N  34637  pl42lem1N  34650  lhpexle3lem  34682  lhpmcvr5N  34698  lhp2atne  34705  lhp2at0ne  34707  4atexlemswapqr  34734  4atexlemex6  34745  ldilco  34787  ltrneq  34820  trlval2  34834  trlnidat  34844  cdlemd2  34870  cdlemd7  34875  cdlemd8  34876  cdleme7aa  34913  cdleme7c  34916  cdleme7d  34917  cdleme7e  34918  cdleme7ga  34919  cdleme7  34920  cdleme11c  34932  cdleme11e  34934  cdleme11l  34940  cdleme11  34941  cdleme14  34944  cdleme15a  34945  cdleme15c  34947  cdleme16b  34950  cdleme16c  34951  cdleme16d  34952  cdleme16e  34953  cdleme16f  34954  cdleme0nex  34961  cdleme18d  34966  cdleme19b  34975  cdleme19d  34977  cdleme19e  34978  cdleme20f  34985  cdleme20i  34988  cdleme20k  34990  cdleme20l1  34991  cdleme20l2  34992  cdleme20l  34993  cdleme20m  34994  cdleme21a  34996  cdleme21b  34997  cdleme21ct  35000  cdleme21d  35001  cdleme21e  35002  cdleme21f  35003  cdleme21h  35005  cdleme22eALTN  35016  cdleme22f2  35018  cdleme22g  35019  cdleme26e  35030  cdleme26eALTN  35032  cdleme26fALTN  35033  cdleme26f  35034  cdleme26f2ALTN  35035  cdleme26f2  35036  cdleme28a  35041  cdleme28b  35042  cdleme28  35044  cdleme29ex  35045  cdleme29c  35047  cdlemefrs29cpre1  35069  cdlemefr29exN  35073  cdlemefr32sn2aw  35075  cdlemefr29bpre0N  35077  cdlemefr29clN  35078  cdlemefr32fvaN  35080  cdlemefr32fva1  35081  cdlemefs32sn1aw  35085  cdleme43fsv1snlem  35091  cdleme41sn3a  35104  cdleme32fva  35108  cdleme32b  35113  cdleme32d  35115  cdleme32e  35116  cdleme32f  35117  cdleme32le  35118  cdleme35a  35119  cdleme35fnpq  35120  cdleme35b  35121  cdleme35c  35122  cdleme35d  35123  cdleme35e  35124  cdleme35f  35125  cdleme36a  35131  cdleme36m  35132  cdleme37m  35133  cdleme39a  35136  cdleme39n  35137  cdleme40m  35138  cdleme40n  35139  cdleme42e  35150  cdleme42f  35151  cdleme42g  35152  cdleme43bN  35161  cdleme43cN  35162  cdleme43dN  35163  cdleme46f2g2  35164  cdleme46f2g1  35165  cdleme17d2  35166  cdleme48b  35174  cdleme4gfv  35178  cdlemeg49le  35182  cdlemeg46c  35184  cdlemeg46fvaw  35187  cdlemeg46nlpq  35188  cdlemeg46frv  35196  cdlemeg46rgv  35199  cdlemeg46req  35200  cdlemeg46gfre  35203  cdleme50trn1  35220  cdleme50trn2a  35221  cdleme50trn2  35222  cdleme  35231  cdlemf  35234  trlord  35240  cdlemg2ce  35263  cdlemg7fvbwN  35278  cdlemg7aN  35296  cdlemg10bALTN  35307  cdlemg10a  35311  cdlemg10  35312  cdlemg12d  35317  cdlemg12f  35319  cdlemg12g  35320  cdlemg12  35321  cdlemg13a  35322  cdlemg13  35323  cdlemg17b  35333  cdlemg17dN  35334  cdlemg17dALTN  35335  cdlemg17e  35336  cdlemg17f  35337  cdlemg17g  35338  cdlemg17h  35339  cdlemg17i  35340  cdlemg17pq  35343  cdlemg17bq  35344  cdlemg17iqN  35345  cdlemg17  35348  cdlemg18d  35352  cdlemg18  35353  cdlemg19a  35354  cdlemg19  35355  cdlemg21  35357  cdlemg27a  35363  cdlemg28a  35364  cdlemg31b0N  35365  cdlemg27b  35367  cdlemg33b0  35372  cdlemg28b  35374  cdlemg28  35375  cdlemg33a  35377  cdlemg33  35382  cdlemg34  35383  cdlemg35  35384  cdlemg36  35385  ltrnco  35390  trlcone  35399  cdlemg44  35404  cdlemg47  35407  cdlemg48  35408  tendococl  35443  tendoplcl  35452  cdlemh1  35486  cdlemi  35491  cdlemj1  35492  cdlemj2  35493  tendocan  35495  cdlemk6  35508  cdlemki  35512  cdlemksat  35517  cdlemksv2  35518  cdlemk7  35519  cdlemk11  35520  cdlemk12  35521  cdlemkoatnle  35522  cdlemkole  35524  cdlemk14  35525  cdlemk15  35526  cdlemk16a  35527  cdlemk16  35528  cdlemk17  35529  cdlemk1u  35530  cdlemk5u  35532  cdlemk6u  35533  cdlemkuat  35537  cdlemk18  35539  cdlemk19  35540  cdlemk12u  35543  cdlemk21N  35544  cdlemk20  35545  cdlemkoatnle-2N  35546  cdlemk13-2N  35547  cdlemkole-2N  35548  cdlemk14-2N  35549  cdlemk15-2N  35550  cdlemk16-2N  35551  cdlemk17-2N  35552  cdlemk18-2N  35557  cdlemk19-2N  35558  cdlemk7u-2N  35559  cdlemk11u-2N  35560  cdlemk12u-2N  35561  cdlemk21-2N  35562  cdlemk20-2N  35563  cdlemk22  35564  cdlemk23-3  35573  cdlemk25-3  35575  cdlemk26b-3  35576  cdlemk27-3  35578  cdlemk28-3  35579  cdlemk33N  35580  cdlemk37  35585  cdlemky  35597  cdlemk11ta  35600  cdlemkid3N  35604  cdlemk11tc  35616  cdlemk11t  35617  cdlemk45  35618  cdlemk46  35619  cdlemk47  35620  cdlemk48  35621  cdlemk49  35622  cdlemk50  35623  cdlemk51  35624  cdlemk52  35625  cdlemk55b  35631  cdlemkyyN  35633  cdlemk55u1  35636  cdlemk55u  35637  cdlemk39u1  35638  cdlemk39u  35639  cdlemk56  35642  cdleml3N  35649  cdleml4N  35650  cdlemm10N  35790  dihord1  35890  dihord2a  35891  dihord2b  35892  dihord10  35895  dihord11c  35896  dihord2pre  35897  dihord4  35930  dihord5apre  35934  dihmeetlem1N  35962  dihglbcpreN  35972  dihjatc1  35983  dihjatc3  35985  dihmeetlem13N  35991  dihmeetlem20N  35998  baerlem3lem2  36382  baerlem5alem2  36383  baerlem5blem2  36384  hdmap14lem11  36553  hdmap14lem12  36554
  Copyright terms: Public domain W3C validator