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

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

Proof of Theorem simp3ll
StepHypRef Expression
1 simpll 758 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  ph )
213ad2ant3 1028 1  |-  ( ( th  /\  ta  /\  ( ( ph  /\  ps )  /\  ch )
)  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  f1oiso2  6249  omeu  7285  ntrivcvgmul  13925  tsmsxp  21093  tgqioo  21722  ovolunlem2  22325  plyadd  23036  plymul  23037  coeeu  23044  tghilberti2  24539  btwnconn1lem2  30637  btwnconn1lem3  30638  btwnconn1lem12  30647  athgt  32730  2llnjN  32841  4atlem12b  32885  lncmp  33057  cdlema2N  33066  cdlemc2  33467  cdleme5  33515  cdleme11a  33535  cdleme21ct  33605  cdleme21  33613  cdleme22eALTN  33621  cdleme24  33628  cdleme27cl  33642  cdleme27a  33643  cdleme28  33649  cdleme36a  33736  cdleme42b  33754  cdleme48fvg  33776  cdlemf  33839  cdlemk39  34192  cdlemkid1  34198  dihlsscpre  34511  dihord4  34535  dihord5apre  34539  dihmeetlem20N  34603  mapdh9a  35067  pellex  35389  jm2.27  35573
  Copyright terms: Public domain W3C validator