Theorem 3simpc 981

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 968	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 979	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 120	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  simp3  984  3adant1  1000  3adantl1  1138  3adantr1  1141  eupickb  2081  find  4521  fisseneq  6828  eqsupti  6891  divcanap2  8464  diveqap0  8466  divrecap  8472  divcanap3  8482  eliooord  9741  fzrev3  9898  sqdivap  10388  muldvds2  11555  dvdscmul  11556  dvdsmulc  11557  dvdstr  11566  cncfmptc  12790  cnplimclemr  12846