Theorem 3simpa 785

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 777	. 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 775

This theorem is referenced by:  3simpb 786  3simpc 787  3simp1 788  3simp2 789  3adant3 799  oaord 4181  lt2halvest 6042  bl2in 7843  methausi 7881  lmle 7960  ajfval 8469  leopmult 10067  strlem3a 10179  fillsb 10560  rcfpfillem3 10589  rcfpfillem3OLD 10590  mslb1 10629  2wsms 10630  msra3 10631  cmpassoh 10729  homgrf 10730  cmpmon 10743  icmpmon 10744

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