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

Theorem simpll3 1049
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simpll3  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )

Proof of Theorem simpll3
StepHypRef Expression
1 simpl3 1013 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 987
This theorem is referenced by:  f1prex  6182  ordiso2  8030  wemappo  8064  iunfictbso  8545  fin1a2lem12  8841  fin1a2lem13  8842  prlem934  9458  ifle  11490  xlesubadd  11549  icoshftf1o  11755  elfzonelfzo  12011  fsuppmapnn0fiub0  12205  swrdcl  12775  repswccat  12888  subcn2  13658  rpdvds  14676  coprmprod  14678  qexpz  14846  ramval  14960  ramvalOLD  14961  0ram  14978  cshwrepswhash1  15073  mreexexd  15554  gsumccat  16625  gsmsymgreqlem1  17071  pmtrf  17096  odmulg  17207  pgpfi1  17247  lsmcl  18306  lbsextlem3  18383  coe1mul2  18862  islindf4  19396  cramerlem2  19713  cpmadugsumlemF  19900  cayhamlem4  19912  iscnp4  20279  cnpnei  20280  cnconst2  20299  cnpdis  20309  cnhaus  20370  ordthauslem  20399  clscon  20445  nlly2i  20491  txcn  20641  ordthmeolem  20816  flimrest  20998  isfcf  21049  alexsubALTlem4  21065  ghmcnp  21129  utop2nei  21265  blssps  21439  blss  21440  metcnp3  21555  metcnp  21556  xrsxmet  21827  metdseq0  21871  metdseq0OLD  21886  xrhmeo  21974  cfil3i  22239  caucfil  22253  cfilres  22266  fta1b  23120  mumul  24108  lgsfcl2  24230  lgsdir  24258  lgsne0  24261  istrkgcb  24504  axbtwnid  24969  axcontlem2  24995  axcontlem4  24997  axcontlem7  25000  axcontlem8  25001  pjhthmo  26955  xrge0adddir  28455  archiabl  28515  pcmplfinf  28688  probun  29252  cnpcon  29953  outsideofeq  30897  linethru  30920  atlatmstc  32885  cvlcvr1  32905  ishlat3N  32920  hlrelat  32967  intnatN  32972  cvrval5  32980  atcvrlln  33085  llnexatN  33086  2at0mat0  33090  llncvrlpln  33123  lplnexllnN  33129  lplncvrlvol  33181  lncvrelatN  33346  pmapjoin  33417  pmapjat1  33418  pclclN  33456  osumclN  33532  lhprelat3N  33605  cdlemd5  33768  cdleme32fvcl  34007  cdlemg39  34283  ltrncom  34305  dihmeetALTN  34895  dochss  34933  mapdrvallem2  35213  nacsfix  35554  mzpsubst  35590  diophrw  35601  lzunuz  35610  jm2.19  35848  jm2.27  35863  hbtlem5  35987  iunrelexpuztr  36311  rfcnnnub  37357  3adantll2  37364  iccintsng  37624  mullimc  37696  mullimcf  37703  limcperiod  37708  cncfshift  37751  cncfperiod  37756  icccncfext  37765  stoweidlem20  37880  stoweidlem61  37922  fourierdlem73  38043  umgr2v2enb1  39563  rmsupp0  40206  rmsuppss  40208
  Copyright terms: Public domain W3C validator