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

Theorem simpll1 1048
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 1012 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ph )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 986
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 189  df-an 373  df-3an 988
This theorem is referenced by:  f1prex  6187  ordiso2  8035  hartogslem1  8062  wemappo  8069  wemapso2lem  8072  acndom  8487  fin1a2lem12  8846  fin1a2lem13  8847  prlem934  9463  ifle  11497  lcmfunsnlem2lem1  14623  rpexp  14684  qexpz  14858  ramval  14972  ramvalOLD  14973  0ram  14990  ramz2  14994  initoeu2lem2  15922  mrelatglb  16442  odbezout  17221  lsmcl  18318  lbsextlem3  18395  psropprmul  18843  coe1mul2  18874  coe1fzgsumdlem  18907  evl1gsumdlem  18956  frlmsslsp  19366  islindf4  19408  scmate  19547  mdetunilem7  19655  mdetmul  19660  cramerlem2  19725  m2pmfzgsumcl  19784  decpmatmul  19808  pmatcollpw3lem  19819  chpdmatlem2  19875  cpmadugsumlemB  19910  cpmadugsumlemC  19911  cpmadugsumlemF  19912  chcoeffeqlem  19921  cnconst2  20311  ordthauslem  20411  clscon  20457  restnlly  20509  comppfsc  20559  ptpjopn  20639  trfg  20918  rnelfmlem  20979  isfcf  21061  fcfnei  21062  cnpfcf  21068  utop2nei  21277  neipcfilu  21323  blssps  21451  blss  21452  metcnp  21568  xrsxmet  21839  metdsge  21878  metdseq0  21883  metdsgeOLD  21893  metdseq0OLD  21898  addcnlem  21908  xrhmeo  21986  nmhmcn  22146  caucfil  22265  limcfval  22839  fta1b  23132  lgsmod  24261  lgsdir  24270  lgsne0  24273  axpasch  24983  axcontlem2  25007  clwwlknwwlkncl  25540  clwlkf1clwwlk  25590  pjhthmo  26967  difioo  28376  xrge0adddir  28467  archiabl  28527  rhmdvdsr  28593  probun  29264  trisegint  30807  btwnconn1lem13  30878  brsegle2  30888  linethru  30932  hlrelat  32979  intnatN  32984  lnnat  33004  3dim0  33034  3dim1  33044  3dim2  33045  atcvrlln  33097  llnexatN  33098  2at0mat0  33102  llncvrlpln  33135  lplnexllnN  33141  lplncvrlvol  33193  lncvrelatN  33358  lncmp  33360  elpaddn0  33377  paddasslem5  33401  pmapjoin  33429  pmapjat1  33430  pclclN  33468  osumclN  33544  lhprelat3N  33617  trlval4  33766  cdlemd5  33780  cdleme32fvcl  34019  cdleme42keg  34065  cdlemg1a  34149  cdlemg1cN  34166  cdlemg39  34295  ltrncom  34317  cdlemk34  34489  dihord2pre  34805  dihopelvalcpre  34828  dihmeetALTN  34907  dihlspsnssN  34912  dihlspsnat  34913  diophrw  35613  lzunuz  35622  qirropth  35768  jm2.19  35860  jm2.27  35875  lmhmfgsplit  35956  hbtlem5  35999  iunrelexpuztr  36323  rfcnnnub  37367  3adantll2  37374  3adantll3  37375  ioondisj2  37599  ioondisj1  37600  iccintsng  37634  icccncfext  37775  stoweidlem20  37890  stoweidlem61  37932  rmsupp0  40257  rmsuppss  40259  ply1mulgsum  40286
  Copyright terms: Public domain W3C validator