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

Theorem simpll2 1036
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 1000 . 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 973
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 975
This theorem is referenced by:  wemappo  7975  iunfictbso  8496  fin1a2lem13  8793  prlem934  9412  ifle  11397  ixxlb  11552  elfzonelfzo  11881  swrdcl  12612  subcn2  13383  qexpz  14282  mreexexd  14906  issubmnd  15770  gsumccat  15844  pmtrf  16295  pgpssslw  16449  lsmmod  16508  reslmhm2b  17512  lsmcl  17541  lbsextlem3  17618  coe1mul2  18121  coe1fzgsumdlem  18154  evl1gsumdlem  18203  frlmsslsp  18636  frlmsslspOLD  18637  islindf4  18680  scmate  18819  mdetdiaglem  18907  madurid  18953  cramerlem2  18997  pmatcollpw3lem  19091  iscnp4  19570  cnrest2  19593  ordthauslem  19690  cncmp  19698  clscon  19737  rnelfmlem  20280  flimrest  20311  isfcf  20362  cnpfcf  20369  alexsubALT  20378  cldsubg  20436  utop2nei  20580  neipcfilu  20626  blssps  20754  blss  20755  stdbdbl  20847  metcnp3  20870  nmoeq0  21070  xrsxmet  21141  metdseq0  21185  addcnlem  21195  xrhmeo  21273  nmhmcn  21430  cfilres  21562  lgsfcl2  23402  lgsdir  23430  lgsne0  23433  istrkgcb  23678  axcontlem2  24041  axcontlem7  24046  axcontlem8  24047  usg2spot2nb  24839  pjhthmo  25993  xrge0adddir  27441  probun  28109  trisegint  29531  btwnconn1lem13  29602  outsideoftr  29632  outsideofeq  29633  linethru  29656  mzpsubst  30512  lzunuz  30532  acongeq  30752  jm2.19  30766  jm2.27  30781  aomclem6  30836  lmhmfgsplit  30863  hbtlem5  30908  3adantll3  31227  ioondisj2  31316  ioondisj1  31317  iccintsng  31354  icccncfext  31453  stoweidlem61  31588  fourierdlem42  31676  fourierdlem73  31707  domnmsuppn0  32260  lincresunit3  32380  atlatmstc  34333  cvlcvr1  34353  hlrelat  34415  intnatN  34420  cvrval5  34428  2at0mat0  34538  llncvrlpln  34571  lplnexllnN  34577  lplncvrlvol  34629  lncvrelatN  34794  lncmp  34796  paddasslem5  34837  pmapjoin  34865  pmapjat1  34866  pclclN  34904  lhprelat3N  35053  cdleme32fvcl  35453  cdlemg1a  35583  cdlemg1cN  35600  cdlemg39  35729  ltrncom  35751  dihmeetALTN  36341  dihlspsnat  36347  mapdrvallem2  36659
  Copyright terms: Public domain W3C validator