Theorem simpll2 1040

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)

Assertion

Ref	Expression
simpll2	|- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem simpll2

Step	Hyp	Ref	Expression
1		simpl2 1004	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-3an 983

This theorem is referenced by:  fidceq  6966  fidifsnen  6967  en2eqpr  7004  iunfidisj  7048  ctssdc  7215  cauappcvgprlemlol  7760  caucvgprlemlol  7783  caucvgprprlemlol  7811  elfzonelfzo  10359  qbtwnre  10399  nn0ltexp2  10854  hashun  10950  swrdclg  11103  xrmaxltsup  11569  subcn2  11622  prodmodclem2  11888  divalglemex  12233  divalglemeuneg  12234  dvdslegcd  12285  lcmledvds  12392  modprmn0modprm0  12579  qexpz  12675  rnglidlmcl  14242  iscnp4  14690  cnrest2  14708  blssps  14899  blss  14900  bdbl  14975  metcnp3  14983  addcncntoplem  15033  cdivcncfap  15076  lgsfcl2  15483  lgsdir  15512  lgsne0  15515