Theorem 3simpa 783

Description: Simplification of triple conjunction.

Assertion

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

Proof of Theorem 3simpa

Step	Hyp	Ref	Expression
1		df-3an 775	. 2 |- ((ph /\ ps /\ ch) <-> ((ph /\ ps) /\ ch))
2	1	pm3.26bi 322	1 |- ((ph /\ ps /\ ch) -> (ph /\ ps))

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

This theorem is referenced by:  3simpb 784  3simpc 785  3simp1 786  3simp2 787  3adant3 797  oaord 4165  lt2halvest 5989  bl2in 7783  methausi 7820  lmle 7895  ajfval 8400  leopmult 9979  strlem3a 10089  fillsb 10435  mslb1 10473  2wsms 10474  msra3 10475  cmpassoh 10573  homgrf 10574  cmpmon 10585  icmpmon 10587

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 775

Copyright terms: Public domain