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

Theorem simpl2l 1008
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 981 . 2  |-  ( ( ch  /\  ( ph  /\ 
ps )  /\  th )  ->  ph )
21adantr 451 1  |-  ( ( ( ch  /\  ( ph  /\  ps )  /\  th )  /\  ta )  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  soisores  5840  omopth2  6598  fin23lem11  7959  xaddass  10585  pockthg  12969  efgred  15073  uncon  17171  basqtop  17418  cxple2  20060  cxple2a  20062  cvmlift2lem10  23858  dedekind  24097  br4  24186  ax5seglem1  24628  ax5seglem2  24629  axpasch  24641  axcontlem4  24667  cgrcomim  24684  btwnintr  24714  btwnouttr2  24717  btwndiff  24722  btwnconn1lem14  24795  btwnconn3  24798  segcon2  24800  brsegle  24803  brsegle2  24804  segleantisym  24810  seglelin  24811  outsideofeu  24826  iccss3  25237  cmprltr  25513  islimrs4  25685  idmon  25920  isconcl5ab  26205  qirropth  27096  mzpcong  27162  jm2.25lem1  27194  jm2.26  27198  idomsubgmo  27617  eqlkr  29911  eqlkr2  29912  lkrlsp  29914  atbtwn  30257  athgt  30267  3dimlem3  30272  3dimlem3OLDN  30273  3dim3  30280  3atlem7  30300  4atlem0a  30404  4atlem3a  30408  4atlem11  30420  lneq2at  30589  lnatexN  30590  cdlemb  30605  paddasslem6  30636  llnexchb2  30680  lhp2lt  30812  lhpexle2lem  30820  lhpexle3  30823  lhpmcvr3  30836  lhpat3  30857  ltrnnidn  30985  ltrneq3  31019  cdleme17b  31098  cdleme25a  31164  cdleme25dN  31167  cdleme27cl  31177  cdlemefrs29bpre0  31207  cdlemefs32sn1aw  31225  cdleme32le  31258  cdleme46f2g2  31304  cdleme46f2g1  31305  cdleme50trn3  31364  trlord  31380  ltrniotavalbN  31395  cdlemg6  31434  cdlemg7N  31437  cdlemg11b  31453  cdlemg15a  31466  cdlemg15  31467  cdlemg39  31527  trlcone  31539  cdlemg42  31540  tendoconid  31640  tendotr  31641  cdlemk39u  31779  cdlemk19u  31781  cdleml5N  31791  cdlemm10N  31930  dihord11b  32034  dihord2pre  32037  dihvalcqpre  32047  dihopelvalcpre  32060  dihord6apre  32068  dihord4  32070  dihord5b  32071  dihglblem5apreN  32103  dihmeetlem13N  32131  dihmeetlem19N  32137  dih1dimatlem0  32140
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator