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

Theorem simp-6l 778
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 776 . 2  |-  ( ( ( ( ( (
ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  ->  ph )
21adantr 466 1  |-  ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  ->  ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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
This theorem is referenced by:  simp-7l  780  ghmcmn  17407  ustuqtop2  21188  ustuqtop4  21190  cnheibor  21879  miriso  24574  f1otrg  24747  txomap  28500  pstmxmet  28539  omssubadd  28961  signstfvneq0  29249  iunconlem2  36972  suplesup  37171  limcleqr  37297  0ellimcdiv  37302  limclner  37304  fourierdlem51  37589
  Copyright terms: Public domain W3C validator