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

Theorem simpll1 1033
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 997 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 463 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  ordiso2  7855  hartogslem1  7882  wemappo  7889  wemapso2lem  7893  acndom  8345  fin1a2lem12  8704  fin1a2lem13  8705  prlem934  9322  ifle  11317  rpexp  14263  qexpz  14422  ramval  14528  0ram  14540  ramz2  14544  initoeu2lem2  15411  mrelatglb  15931  odbezout  16697  lsmcl  17842  lbsextlem3  17919  psropprmul  18392  coe1mul2  18423  coe1fzgsumdlem  18456  evl1gsumdlem  18505  frlmsslsp  18916  islindf4  18958  scmate  19097  mdetunilem7  19205  mdetmul  19210  cramerlem2  19275  m2pmfzgsumcl  19334  decpmatmul  19358  pmatcollpw3lem  19369  chpdmatlem2  19425  cpmadugsumlemB  19460  cpmadugsumlemC  19461  cpmadugsumlemF  19462  chcoeffeqlem  19471  cnconst2  19870  ordthauslem  19970  clscon  20016  restnlly  20068  comppfsc  20118  ptpjopn  20198  trfg  20477  rnelfmlem  20538  isfcf  20620  fcfnei  20621  cnpfcf  20627  utop2nei  20838  neipcfilu  20884  blssps  21012  blss  21013  metcnp  21129  xrsxmet  21399  metdsge  21438  metdseq0  21443  addcnlem  21453  xrhmeo  21531  nmhmcn  21688  caucfil  21807  limcfval  22361  fta1b  22655  lgsmod  23713  lgsdir  23722  lgsne0  23725  axpasch  24365  axcontlem2  24389  clwwlknwwlkncl  24921  clwlkf1clwwlk  24971  pjhthmo  26337  difioo  27746  xrge0adddir  27835  archiabl  27895  rhmdvdsr  27962  probun  28541  trisegint  29831  btwnconn1lem13  29902  brsegle2  29912  linethru  29956  diophrw  30857  lzunuz  30866  qirropth  31009  jm2.19  31101  jm2.27  31116  lmhmfgsplit  31198  hbtlem5  31245  rfcnnnub  31578  3adantll2  31587  3adantll3  31588  ioondisj2  31691  ioondisj1  31692  iccintsng  31729  icccncfext  31856  stoweidlem20  31968  stoweidlem61  32009  rmsupp0  33161  rmsuppss  33163  ply1mulgsum  33190  hlrelat  35539  intnatN  35544  lnnat  35564  3dim0  35594  3dim1  35604  3dim2  35605  atcvrlln  35657  llnexatN  35658  2at0mat0  35662  llncvrlpln  35695  lplnexllnN  35701  lplncvrlvol  35753  lncvrelatN  35918  lncmp  35920  elpaddn0  35937  paddasslem5  35961  pmapjoin  35989  pmapjat1  35990  pclclN  36028  osumclN  36104  lhprelat3N  36177  trlval4  36326  cdlemd5  36340  cdleme32fvcl  36579  cdleme42keg  36625  cdlemg1a  36709  cdlemg1cN  36726  cdlemg39  36855  ltrncom  36877  cdlemk34  37049  dihord2pre  37365  dihopelvalcpre  37388  dihmeetALTN  37467  dihlspsnssN  37472  dihlspsnat  37473  iunrelexpuztr  38224
  Copyright terms: Public domain W3C validator