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

Theorem simpll3 1032
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 996 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ch )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ch )
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  wemappo  7963  iunfictbso  8484  fin1a2lem12  8780  fin1a2lem13  8781  prlem934  9400  ifle  11385  xlesubadd  11444  icoshftf1o  11632  elfzonelfzo  11869  fsuppmapnn0fiub0  12055  swrdcl  12596  repswccat  12707  subcn2  13366  rpdvds  14113  qexpz  14268  ramval  14374  0ram  14386  cshwrepswhash1  14434  mreexexd  14892  gsumccat  15825  gsmsymgreqlem1  16243  pmtrf  16269  odmulg  16367  pgpfi1  16404  lsmcl  17505  lbsextlem3  17582  coe1mul2  18074  islindf4  18633  cramerlem2  18950  cpmadugsumlemF  19137  cayhamlem4  19149  iscnp4  19523  cnpnei  19524  cnconst2  19543  cnpdis  19553  cnhaus  19614  ordthauslem  19643  clscon  19690  nlly2i  19736  txcn  19855  ordthmeolem  20030  flimrest  20212  isfcf  20263  alexsubALTlem4  20278  ghmcnp  20341  utop2nei  20481  blssps  20655  blss  20656  metcnp3  20771  metcnp  20772  xrsxmet  21042  metdseq0  21086  xrhmeo  21174  cfil3i  21436  caucfil  21450  cfilres  21463  fta1b  22298  mumul  23176  lgsfcl2  23298  lgsdir  23326  lgsne0  23329  istrkgcb  23574  axbtwnid  23911  axcontlem2  23937  axcontlem4  23939  axcontlem7  23942  axcontlem8  23943  pjhthmo  25882  xrge0adddir  27330  archiabl  27390  probun  27984  cnpcon  28301  outsideofeq  29343  linethru  29366  nacsfix  30235  mzpsubst  30272  diophrw  30283  lzunuz  30292  jm2.19  30528  jm2.27  30543  hbtlem5  30670  rfcnnnub  30944  3adantll2  30954  iccintsng  31082  mullimc  31113  mullimcf  31120  limcperiod  31125  cncfshift  31167  cncfperiod  31172  icccncfext  31181  stoweidlem20  31275  stoweidlem61  31316  fourierdlem73  31435  rmsupp0  31909  rmsuppss  31911  atlatmstc  33991  cvlcvr1  34011  ishlat3N  34026  hlrelat  34073  intnatN  34078  cvrval5  34086  atcvrlln  34191  llnexatN  34192  2at0mat0  34196  llncvrlpln  34229  lplnexllnN  34235  lplncvrlvol  34287  lncvrelatN  34452  pmapjoin  34523  pmapjat1  34524  pclclN  34562  osumclN  34638  lhprelat3N  34711  cdlemd5  34873  cdleme32fvcl  35111  cdlemg39  35387  ltrncom  35409  dihmeetALTN  35999  dochss  36037  mapdrvallem2  36317
  Copyright terms: Public domain W3C validator