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

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

Proof of Theorem simpll2
StepHypRef Expression
1 simpl2 999 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 465 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 972
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 974
This theorem is referenced by:  wemappo  7972  iunfictbso  8493  fin1a2lem13  8790  prlem934  9409  ifle  11400  ixxlb  11555  elfzonelfzo  11886  swrdcl  12620  subcn2  13391  qexpz  14292  mreexexd  14917  issubmnd  15817  gsumccat  15878  frmdup3lem  15903  pmtrf  16349  pgpssslw  16503  lsmmod  16562  reslmhm2b  17568  lsmcl  17597  lbsextlem3  17674  coe1mul2  18178  coe1fzgsumdlem  18211  evl1gsumdlem  18260  frlmsslsp  18696  frlmsslspOLD  18697  islindf4  18740  scmate  18879  mdetdiaglem  18967  madurid  19013  cramerlem2  19057  pmatcollpw3lem  19151  iscnp4  19630  cnrest2  19653  ordthauslem  19750  cncmp  19758  clscon  19797  rnelfmlem  20319  flimrest  20350  isfcf  20401  cnpfcf  20408  alexsubALT  20417  cldsubg  20475  utop2nei  20619  neipcfilu  20665  blssps  20793  blss  20794  stdbdbl  20886  metcnp3  20909  nmoeq0  21109  xrsxmet  21180  metdseq0  21224  addcnlem  21234  xrhmeo  21312  nmhmcn  21469  cfilres  21601  lgsfcl2  23442  lgsdir  23470  lgsne0  23473  istrkgcb  23718  axcontlem2  24133  axcontlem7  24138  axcontlem8  24139  usg2spot2nb  24930  pjhthmo  26085  xrge0adddir  27548  pcmplfinf  27730  probun  28224  trisegint  29646  btwnconn1lem13  29717  outsideoftr  29747  outsideofeq  29748  linethru  29771  mzpsubst  30649  lzunuz  30669  acongeq  30889  jm2.19  30903  jm2.27  30918  aomclem6  30973  lmhmfgsplit  31000  hbtlem5  31045  3adantll3  31369  ioondisj2  31457  ioondisj1  31458  iccintsng  31495  icccncfext  31593  stoweidlem61  31728  fourierdlem42  31816  fourierdlem73  31847  domnmsuppn0  32672  lincresunit3  32792  atlatmstc  34746  cvlcvr1  34766  hlrelat  34828  intnatN  34833  cvrval5  34841  2at0mat0  34951  llncvrlpln  34984  lplnexllnN  34990  lplncvrlvol  35042  lncvrelatN  35207  lncmp  35209  paddasslem5  35250  pmapjoin  35278  pmapjat1  35279  pclclN  35317  lhprelat3N  35466  cdleme32fvcl  35868  cdlemg1a  35998  cdlemg1cN  36015  cdlemg39  36144  ltrncom  36166  dihmeetALTN  36756  dihlspsnat  36762  mapdrvallem2  37074
  Copyright terms: Public domain W3C validator