Theorem 3simpc 986

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

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

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 970

This theorem is referenced by:  simp3  989  3adant1  1005  3adantl1  1143  3adantr1  1146  eupickb  2095  find  4576  fisseneq  6897  eqsupti  6961  divcanap2  8576  diveqap0  8578  divrecap  8584  divcanap3  8594  eliooord  9864  fzrev3  10022  sqdivap  10519  muldvds2  11757  dvdscmul  11758  dvdsmulc  11759  dvdstr  11768  cncfmptc  13222  cnplimclemr  13278