Theorem simpll3 1041

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

Assertion

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

Proof of Theorem simpll3

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

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  ax-ia3 108

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

This theorem is referenced by:  frirrg  4397  fidceq  6966  fidifsnen  6967  en2eqpr  7004  iunfidisj  7048  ordiso2  7137  addlocpr  7649  aptiprlemu  7753  xltadd1  9998  xlesubadd  10005  icoshftf1o  10113  fztri3or  10161  elfzonelfzo  10359  exp3val  10686  nn0ltexp2  10854  hashun  10950  swrdclg  11103  subcn2  11622  divalglemeuneg  12234  dvdslegcd  12285  lcmledvds  12392  rpdvds  12421  cncongr2  12426  qexpz  12675  iuncld  14587  iscnp4  14690  cnpnei  14691  cnconst2  14705  cnpdis  14714  txcn  14747  blssps  14899  blss  14900  metcnp3  14983  metcnp  14984  lgsfcl2  15483  lgsdir  15512  lgsne0  15515