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

Theorem simpll1 1036
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )

Proof of Theorem simpll1
StepHypRef Expression
1 simpl1 1000 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ 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:  ordiso2  7943  hartogslem1  7970  wemappo  7977  wemapso2lem  7981  acndom  8435  fin1a2lem12  8794  fin1a2lem13  8795  prlem934  9414  ifle  11406  rpexp  14242  qexpz  14401  ramval  14507  0ram  14519  ramz2  14523  mrelatglb  15792  odbezout  16558  lsmcl  17707  lbsextlem3  17784  psropprmul  18257  coe1mul2  18288  coe1fzgsumdlem  18321  evl1gsumdlem  18370  frlmsslsp  18806  frlmsslspOLD  18807  islindf4  18850  scmate  18989  mdetunilem7  19097  mdetmul  19102  cramerlem2  19167  m2pmfzgsumcl  19226  decpmatmul  19250  pmatcollpw3lem  19261  chpdmatlem2  19317  cpmadugsumlemB  19352  cpmadugsumlemC  19353  cpmadugsumlemF  19354  chcoeffeqlem  19363  cnconst2  19761  ordthauslem  19861  clscon  19908  restnlly  19960  comppfsc  20010  ptpjopn  20090  trfg  20369  rnelfmlem  20430  isfcf  20512  fcfnei  20513  cnpfcf  20519  utop2nei  20730  neipcfilu  20776  blssps  20904  blss  20905  metcnp  21021  xrsxmet  21291  metdsge  21330  metdseq0  21335  addcnlem  21345  xrhmeo  21423  nmhmcn  21580  caucfil  21699  limcfval  22253  fta1b  22547  lgsmod  23572  lgsdir  23581  lgsne0  23584  axpasch  24220  axcontlem2  24244  clwwlknwwlkncl  24776  clwlkf1clwwlk  24826  pjhthmo  26196  difioo  27569  xrge0adddir  27659  archiabl  27719  rhmdvdsr  27785  probun  28335  trisegint  29653  btwnconn1lem13  29724  brsegle2  29734  linethru  29778  diophrw  30667  lzunuz  30676  qirropth  30819  jm2.19  30910  jm2.27  30925  lmhmfgsplit  31007  hbtlem5  31052  rfcnnnub  31365  3adantll2  31374  3adantll3  31375  ioondisj2  31461  ioondisj1  31462  iccintsng  31499  icccncfext  31597  stoweidlem20  31691  stoweidlem61  31732  rmsupp0  32696  rmsuppss  32698  ply1mulgsum  32725  hlrelat  34866  intnatN  34871  lnnat  34891  3dim0  34921  3dim1  34931  3dim2  34932  atcvrlln  34984  llnexatN  34985  2at0mat0  34989  llncvrlpln  35022  lplnexllnN  35028  lplncvrlvol  35080  lncvrelatN  35245  lncmp  35247  elpaddn0  35264  paddasslem5  35288  pmapjoin  35316  pmapjat1  35317  pclclN  35355  osumclN  35431  lhprelat3N  35504  trlval4  35653  cdlemd5  35667  cdleme32fvcl  35906  cdleme42keg  35952  cdlemg1a  36036  cdlemg1cN  36053  cdlemg39  36182  ltrncom  36204  cdlemk34  36376  dihord2pre  36692  dihopelvalcpre  36715  dihmeetALTN  36794  dihlspsnssN  36799  dihlspsnat  36800
  Copyright terms: Public domain W3C validator