Theorem simpll2 1068

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 1032	. 2 |- ( ( ( ph /\ ps /\ ch ) /\ th ) -> ps )
2	1	adantr 276	1 |- ( ( ( ( ph /\ ps /\ ch ) /\ th ) /\ ta ) -> ps )

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

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 1011

This theorem is referenced by:  fidceq  7161  fidifsnen  7162  en2eqpr  7204  iunfidisj  7250  fdcf1  7306  ctssdc  7443  cauappcvgprlemlol  8004  caucvgprlemlol  8027  caucvgprprlemlol  8055  elfzonelfzo  10626  qbtwnre  10669  nn0ltexp2  11125  hashun  11223  swrdclg  11400  xrmaxltsup  12002  subcn2  12055  prodmodclem2  12322  divalglemex  12667  divalglemeuneg  12668  dvdslegcd  12719  lcmledvds  12826  modprmn0modprm0  13013  qexpz  13109  rnglidlmcl  14789  iscnp4  15242  cnrest2  15260  blssps  15451  blss  15452  bdbl  15527  metcnp3  15535  addcncntoplem  15585  cdivcncfap  15628  lgsfcl2  16039  lgsdir  16068  lgsne0  16071  subupgr  16428  clwwlknonex2  16594