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

Theorem simpll1 1030
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 994 . 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 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:  ordiso2  7929  hartogslem1  7956  wemappo  7963  wemapso2lem  7967  acndom  8421  fin1a2lem12  8780  fin1a2lem13  8781  prlem934  9400  ifle  11385  rpexp  14109  qexpz  14268  ramval  14374  0ram  14386  ramz2  14390  mrelatglb  15660  odbezout  16369  lsmcl  17505  lbsextlem3  17582  psropprmul  18043  coe1mul2  18074  coe1fzgsumdlem  18107  evl1gsumdlem  18156  frlmsslsp  18589  frlmsslspOLD  18590  islindf4  18633  scmate  18772  mdetunilem7  18880  mdetmul  18885  cramerlem2  18950  m2pmfzgsumcl  19009  decpmatmul  19033  pmatcollpw3lem  19044  chpdmatlem2  19100  cpmadugsumlemB  19135  cpmadugsumlemC  19136  cpmadugsumlemF  19137  chcoeffeqlem  19146  cnconst2  19543  ordthauslem  19643  clscon  19690  restnlly  19742  ptpjopn  19841  trfg  20120  rnelfmlem  20181  isfcf  20263  fcfnei  20264  cnpfcf  20270  utop2nei  20481  neipcfilu  20527  blssps  20655  blss  20656  metcnp  20772  xrsxmet  21042  metdsge  21081  metdseq0  21086  addcnlem  21096  xrhmeo  21174  nmhmcn  21331  caucfil  21450  limcfval  22004  fta1b  22298  lgsmod  23317  lgsdir  23326  lgsne0  23329  axpasch  23913  axcontlem2  23937  clwwlknwwlkncl  24462  clwlkf1clwwlk  24512  pjhthmo  25882  difioo  27247  xrge0adddir  27330  archiabl  27390  rhmdvdsr  27457  probun  27984  trisegint  29241  btwnconn1lem13  29312  brsegle2  29322  linethru  29366  comppfsc  29766  diophrw  30283  lzunuz  30292  qirropth  30435  jm2.19  30528  jm2.27  30543  lmhmfgsplit  30625  hbtlem5  30670  rfcnnnub  30944  3adantll2  30954  3adantll3  30955  ioondisj2  31044  ioondisj1  31045  iccintsng  31082  icccncfext  31181  stoweidlem20  31275  stoweidlem61  31316  rmsupp0  31909  rmsuppss  31911  ply1mulgsum  31938  hlrelat  34073  intnatN  34078  lnnat  34098  3dim0  34128  3dim1  34138  3dim2  34139  atcvrlln  34191  llnexatN  34192  2at0mat0  34196  llncvrlpln  34229  lplnexllnN  34235  lplncvrlvol  34287  lncvrelatN  34452  lncmp  34454  elpaddn0  34471  paddasslem5  34495  pmapjoin  34523  pmapjat1  34524  pclclN  34562  osumclN  34638  lhprelat3N  34711  trlval4  34859  cdlemd5  34873  cdleme32fvcl  35111  cdleme42keg  35157  cdlemg1a  35241  cdlemg1cN  35258  cdlemg39  35387  ltrncom  35409  cdlemk34  35581  dihord2pre  35897  dihopelvalcpre  35920  dihmeetALTN  35999  dihlspsnssN  36004  dihlspsnat  36005
  Copyright terms: Public domain W3C validator