Theorem 3simpc 787

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simpc

Step	Hyp	Ref	Expression
1		3anrot 780	. 2 |- ((ph /\ ps /\ ch) <-> (ps /\ ch /\ ph))
2		3simpa 785	. 2 |- ((ps /\ ch /\ ph) -> (ps /\ ch))
3	1, 2	sylbi 199	1 |- ((ph /\ ps /\ ch) -> (ps /\ ch))

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  3simp3 790  3adant1 797  eupickb 1435  tz7.49c 3960  nnleltp1t 5954  eliooordt 6388  fzrev3t 6514  seqzvalt 6540  ajfuni 8520  psasym 8651  pstr 8652  spwpr4OLD 8663  spwpr4aOLD 8664  funadj 9813  ismonb2 10740  cmpmon 10743  isepib2 10750

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain