Theorem simpll3 917

Description: Simplification of conjunction.

Assertion

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

Proof of Theorem simpll3

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

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858

This theorem is referenced by:  cnpnei 9043  gapmlem 9461  uptx 10226  subtopmetlem 10255  fbfgss 10288  alexsublem4 15440  fnetr 15495  fmufil 15599  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  heiborlem16 15970  hlrelat 17051  pmapjoin 17313  pmapjat 17314  osumcl 17375

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242  df-3an 860

Copyright terms: Public domain