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

Theorem simpll2 1046
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 1010 . 2  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
21adantr 467 1  |-  ( ( ( ( ph  /\  ps  /\  ch )  /\  th )  /\  ta )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 983
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 985
This theorem is referenced by:  f1prex  6195  wemappo  8068  iunfictbso  8547  fin1a2lem13  8844  prlem934  9460  ifle  11492  ixxlb  11659  ixxlbOLD  11660  elfzonelfzo  12012  swrdcl  12771  subcn2  13651  qexpz  14839  mreexexd  15547  initoeu2lem2  15903  issubmnd  16557  gsumccat  16618  frmdup3lem  16643  pmtrf  17089  pgpssslw  17259  lsmmod  17318  reslmhm2b  18270  lsmcl  18299  lbsextlem3  18376  coe1mul2  18855  coe1fzgsumdlem  18888  evl1gsumdlem  18937  frlmsslsp  19346  islindf4  19388  scmate  19527  mdetdiaglem  19615  madurid  19661  cramerlem2  19705  pmatcollpw3lem  19799  iscnp4  20271  cnrest2  20294  ordthauslem  20391  cncmp  20399  clscon  20437  rnelfmlem  20959  flimrest  20990  isfcf  21041  cnpfcf  21048  alexsubALT  21058  cldsubg  21117  utop2nei  21257  neipcfilu  21303  blssps  21431  blss  21432  stdbdbl  21524  metcnp3  21547  nmoeq0  21749  xrsxmet  21819  metdseq0  21863  metdseq0OLD  21878  addcnlem  21888  xrhmeo  21966  nmhmcn  22126  cfilres  22258  lgsfcl2  24222  lgsdir  24250  lgsne0  24253  istrkgcb  24496  axcontlem2  24987  axcontlem7  24992  axcontlem8  24993  usg2spot2nb  25785  pjhthmo  26947  xrge0adddir  28456  pcmplfinf  28690  probun  29254  trisegint  30794  btwnconn1lem13  30865  outsideoftr  30895  outsideofeq  30896  linethru  30919  isbasisrelowllem1  31716  atlatmstc  32848  cvlcvr1  32868  hlrelat  32930  intnatN  32935  cvrval5  32943  2at0mat0  33053  llncvrlpln  33086  lplnexllnN  33092  lplncvrlvol  33144  lncvrelatN  33309  lncmp  33311  paddasslem5  33352  pmapjoin  33380  pmapjat1  33381  pclclN  33419  lhprelat3N  33568  cdleme32fvcl  33970  cdlemg1a  34100  cdlemg1cN  34117  cdlemg39  34246  ltrncom  34268  dihmeetALTN  34858  dihlspsnat  34864  mapdrvallem2  35176  mzpsubst  35553  lzunuz  35573  acongeq  35797  jm2.19  35812  jm2.27  35827  aomclem6  35881  lmhmfgsplit  35908  hbtlem5  35951  iunrelexpuztr  36215  3adantll3  37270  ioondisj2  37464  ioondisj1  37465  iccintsng  37499  icccncfext  37629  stoweidlem61  37786  fourierdlem42  37876  fourierdlem42OLD  37877  fourierdlem73  37907  domnmsuppn0  39498  lincresunit3  39618  nnolog2flm1  39745
  Copyright terms: Public domain W3C validator