Theorem 3impa 609

Description: Importation from double to triple conjunction.

Hypothesis

Ref	Expression
3impa.1	|- (((ph /\ ps) /\ ch) -> th)

Assertion

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

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		3impa.1	. . 3 |- (((ph /\ ps) /\ ch) -> th)
2	1	exp31 293	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 608	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 2   /\ wa 196   /\ w3a 581

This theorem is referenced by:  3impdir 631  syl3an9b 634  rspec3 1268  3optocl 2471  oaword 3151  nnmass 3181  ecoprass 3256  addasspi 3817  mulasspi 3819  ltapi 3824  ltmpi 3825  genpass 3906  axltadd 4085  axsup 4088  adddirt 4103  divasst 4239  le2tri3 4311  ltaddsubt 4357  hvaddsubasst 5018  elspansn2t 5472  cvnbtwnt 5718  mdi 5727  dmdi 5732

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

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583

metamath.org