Theorem 3simpc 1020

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

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

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 1004

This theorem is referenced by:  simp3  1023  3adant1  1039  3adantl1  1177  3adantr1  1180  eupickb  2159  find  4695  fovcld  6121  fisseneq  7119  eqsupti  7186  divcanap2  8850  diveqap0  8852  divrecap  8858  divcanap3  8868  eliooord  10153  fzrev3  10312  sqdivap  10855  swrdlend  11229  swrdnd  11230  ccats1pfxeqbi  11313  muldvds2  12368  dvdscmul  12369  dvdsmulc  12370  dvdstr  12379  domneq0  14276  znleval2  14658  cncfmptc  15310  cnplimclemr  15383  uhgr2edg  16045  umgr2edgneu  16051  clwwlknp  16212