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

Theorem simpll1 1027
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 991 . 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 965
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 967
This theorem is referenced by:  ordiso2  7727  hartogslem1  7754  wemappo  7761  wemapso2lem  7765  acndom  8219  fin1a2lem12  8578  fin1a2lem13  8579  prlem934  9200  ifle  11165  rpexp  13804  qexpz  13961  ramval  14067  0ram  14079  ramz2  14083  mrelatglb  15352  odbezout  16057  lsmcl  17162  lbsextlem3  17239  psropprmul  17691  coe1mul2  17721  evl1gsumdlem  17788  frlmsslsp  18221  frlmsslspOLD  18222  islindf4  18265  mdetunilem7  18422  mdetmul  18427  cramerlem2  18492  cnconst2  18885  ordthauslem  18985  clscon  19032  restnlly  19084  ptpjopn  19183  trfg  19462  rnelfmlem  19523  isfcf  19605  fcfnei  19606  cnpfcf  19612  utop2nei  19823  neipcfilu  19869  blssps  19997  blss  19998  metcnp  20114  xrsxmet  20384  metdsge  20423  metdseq0  20428  addcnlem  20438  xrhmeo  20516  nmhmcn  20673  caucfil  20792  limcfval  21345  fta1b  21639  lgsmod  22658  lgsdir  22667  lgsne0  22670  axpasch  23185  axcontlem2  23209  pjhthmo  24703  difioo  26070  xrge0adddir  26153  archiabl  26213  rhmdvdsr  26284  probun  26800  trisegint  28057  btwnconn1lem13  28128  brsegle2  28138  linethru  28182  comppfsc  28576  diophrw  29094  lzunuz  29103  qirropth  29246  jm2.19  29339  jm2.27  29354  lmhmfgsplit  29436  hbtlem5  29481  rfcnnnub  29755  stoweidlem20  29812  stoweidlem61  29853  clwwlknwwlkncl  30459  clwlkf1clwwlk  30520  rmsupp0  30778  rmsuppss  30780  coe1fzgsumdlem  30834  ply1mulgsum  30845  hlrelat  33043  intnatN  33048  lnnat  33068  3dim0  33098  3dim1  33108  3dim2  33109  atcvrlln  33161  llnexatN  33162  2at0mat0  33166  llncvrlpln  33199  lplnexllnN  33205  lplncvrlvol  33257  lncvrelatN  33422  lncmp  33424  elpaddn0  33441  paddasslem5  33465  pmapjoin  33493  pmapjat1  33494  pclclN  33532  osumclN  33608  lhprelat3N  33681  trlval4  33829  cdlemd5  33843  cdleme32fvcl  34081  cdleme42keg  34127  cdlemg1a  34211  cdlemg1cN  34228  cdlemg39  34357  ltrncom  34379  cdlemk34  34551  dihord2pre  34867  dihopelvalcpre  34890  dihmeetALTN  34969  dihlspsnssN  34974  dihlspsnat  34975
  Copyright terms: Public domain W3C validator