MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simp-6l Structured version   Unicode version

Theorem simp-6l 769
Description: Simplification of a conjunction. (Contributed by Mario Carneiro, 4-Jan-2017.)
Assertion
Ref Expression
simp-6l  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ph )

Proof of Theorem simp-6l
StepHypRef Expression
1 simp-5l 767 . 2  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ph )
21adantr 465 1  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  simp-7l  771  ghmcmn  16655  ustuqtop2  20572  ustuqtop4  20574  cnheibor  21282  miriso  23860  f1otrg  23947  txomap  27597  pstmxmet  27627  signstfvneq0  28280  0ellimcdiv  31418  limclner  31420  icccncfext  31453  fourierdlem51  31685  iunconlem2  33032
  Copyright terms: Public domain W3C validator