Theorem 3simpc 996

Description: Simplification of triple conjunction. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
3simpc	|- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 983	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 994	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 121	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

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

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 980

This theorem is referenced by:  simp3  999  3adant1  1015  3adantl1  1153  3adantr1  1156  eupickb  2107  find  4598  fisseneq  6930  eqsupti  6994  divcanap2  8635  diveqap0  8637  divrecap  8643  divcanap3  8653  eliooord  9926  fzrev3  10084  sqdivap  10581  muldvds2  11819  dvdscmul  11820  dvdsmulc  11821  dvdstr  11830  cncfmptc  13975  cnplimclemr  14031