Theorem simpll1 1100

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll1	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )

Proof of Theorem simpll1

Step	Hyp	Ref	Expression
1		simpl1 1064	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ph )
2	1	adantr 481	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ph )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  f1prex  6539  ordiso2  8420  hartogslem1  8447  wemappo  8454  wemapso2lem  8457  acndom  8874  fin1a2lem12  9233  fin1a2lem13  9234  prlem934  9855  ifle  12028  lcmfunsnlem2lem1  15351  divgcdcoprm0  15379  rpexp  15432  qexpz  15605  ramval  15712  0ram  15724  ramz2  15728  initoeu2lem2  16665  mrelatglb  17184  dfgrp3lem  17513  odbezout  17975  lsmcl  19083  lbsextlem3  19160  psropprmul  19608  coe1mul2  19639  coe1fzgsumdlem  19671  evl1gsumdlem  19720  frlmsslsp  20135  islindf4  20177  scmate  20316  mdetunilem7  20424  mdetmul  20429  cramerlem2  20494  m2pmfzgsumcl  20553  decpmatmul  20577  pmatcollpw3lem  20588  chpdmatlem2  20644  cpmadugsumlemB  20679  cpmadugsumlemC  20680  cpmadugsumlemF  20681  chcoeffeqlem  20690  cnconst2  21087  ordthauslem  21187  clsconn  21233  restnlly  21285  comppfsc  21335  ptpjopn  21415  trfg  21695  rnelfmlem  21756  isfcf  21838  fcfnei  21839  cnpfcf  21845  utop2nei  22054  neipcfilu  22100  blssps  22229  blss  22230  metcnp  22346  xrsxmet  22612  metdsge  22652  metdseq0  22657  addcnlem  22667  xrhmeo  22745  nmhmcn  22920  caucfil  23081  limcfval  23636  fta1b  23929  lgsmod  25048  lgsdir  25057  lgsne0  25060  axpasch  25821  axcontlem2  25845  wpthswwlks2on  26854  clwwlksnwwlkncl  26921  frgr3v  27139  pjhthmo  28161  difioo  29544  xrge0adddir  29692  archiabl  29752  rhmdvdsr  29818  probun  30481  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd2  31862  scutun12  31917  trisegint  32135  btwnconn1lem13  32206  brsegle2  32216  linethru  32260  hlrelat  34688  intnatN  34693  lnnat  34713  3dim0  34743  3dim1  34753  3dim2  34754  atcvrlln  34806  llnexatN  34807  2at0mat0  34811  llncvrlpln  34844  lplnexllnN  34850  lplncvrlvol  34902  lncvrelatN  35067  lncmp  35069  elpaddn0  35086  paddasslem5  35110  pmapjoin  35138  pmapjat1  35139  pclclN  35177  osumclN  35253  lhprelat3N  35326  trlval4  35475  cdlemd5  35489  cdleme32fvcl  35728  cdleme42keg  35774  cdlemg1a  35858  cdlemg1cN  35875  cdlemg39  36004  ltrncom  36026  cdlemk34  36198  dihord2pre  36514  dihopelvalcpre  36537  dihmeetALTN  36616  dihlspsnssN  36621  dihlspsnat  36622  diophrw  37322  lzunuz  37331  qirropth  37473  jm2.19  37560  jm2.27  37575  lmhmfgsplit  37656  hbtlem5  37698  iunrelexpuztr  38011  rfcnnnub  39195  3adantll2  39202  3adantll3  39203  ioondisj2  39714  ioondisj1  39715  iccintsng  39749  icccncfext  40100  stoweidlem20  40237  stoweidlem61  40278  smflimlem2  40980  rmsupp0  42149  rmsuppss  42151  ply1mulgsum  42178