Theorem 3simpc 1023

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 1010	. 2 |- ( ( ph /\ ps /\ ch ) <-> ( ps /\ ch /\ ph ) )
2		3simpa 1021	. 2 |- ( ( ps /\ ch /\ ph ) -> ( ps /\ ch ) )
3	1, 2	sylbi 121	1 |- ( ( ph /\ ps /\ ch ) -> ( ps /\ ch ) )

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

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 1007

This theorem is referenced by:  simp3  1026  3adant1  1042  3adantl1  1180  3adantr1  1183  eupickb  2161  find  4703  fovcld  6136  fisseneq  7170  eqsupti  7238  divcanap2  8902  diveqap0  8904  divrecap  8910  divcanap3  8920  eliooord  10207  fzrev3  10367  sqdivap  10911  swrdlend  11288  swrdnd  11289  ccats1pfxeqbi  11372  muldvds2  12441  dvdscmul  12442  dvdsmulc  12443  dvdstr  12452  domneq0  14351  znleval2  14733  cncfmptc  15390  cnplimclemr  15463  uhgr2edg  16130  umgr2edgneu  16136  clwwlknp  16341