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

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

Proof of Theorem simpl2l
StepHypRef Expression
1 simp2l 983 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantr 452 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  soisores  6047  omopth2  6827  fin23lem11  8197  xaddass  10828  pockthg  13274  efgred  15380  uncon  17492  basqtop  17743  utop2nei  18280  ucncn  18315  cxple2  20588  cxple2a  20590  cvmlift2lem10  24999  dedekind  25187  ntrivcvgmul  25230  br4  25381  ax5seglem1  25867  ax5seglem2  25868  axpasch  25880  axcontlem4  25906  cgrcomim  25923  btwnintr  25953  btwnouttr2  25956  btwndiff  25961  btwnconn1lem14  26034  btwnconn3  26037  segcon2  26039  brsegle  26042  brsegle2  26043  segleantisym  26049  seglelin  26050  outsideofeu  26065  qirropth  26971  mzpcong  27037  jm2.25lem1  27069  jm2.26  27073  idomsubgmo  27491  eqlkr  29897  eqlkr2  29898  lkrlsp  29900  atbtwn  30243  athgt  30253  3dimlem3  30258  3dimlem3OLDN  30259  3dim3  30266  3atlem7  30286  4atlem0a  30390  4atlem3a  30394  4atlem11  30406  lneq2at  30575  lnatexN  30576  cdlemb  30591  paddasslem6  30622  llnexchb2  30666  lhp2lt  30798  lhpexle2lem  30806  lhpexle3  30809  lhpmcvr3  30822  lhpat3  30843  ltrnnidn  30971  ltrneq3  31005  cdleme17b  31084  cdleme25a  31150  cdleme25dN  31153  cdleme27cl  31163  cdlemefrs29bpre0  31193  cdlemefs32sn1aw  31211  cdleme32le  31244  cdleme46f2g2  31290  cdleme46f2g1  31291  cdleme50trn3  31350  trlord  31366  ltrniotavalbN  31381  cdlemg6  31420  cdlemg7N  31423  cdlemg11b  31439  cdlemg15a  31452  cdlemg15  31453  cdlemg39  31513  trlcone  31525  cdlemg42  31526  tendoconid  31626  tendotr  31627  cdlemk39u  31765  cdlemk19u  31767  cdleml5N  31777  cdlemm10N  31916  dihord11b  32020  dihord2pre  32023  dihvalcqpre  32033  dihopelvalcpre  32046  dihord6apre  32054  dihord4  32056  dihord5b  32057  dihglblem5apreN  32089  dihmeetlem13N  32117  dihmeetlem19N  32123  dih1dimatlem0  32126
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator