Theorem 3expb 613

Description: Exportation from triple to double conjunction.

Hypothesis

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

Assertion

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

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 |- ((ph /\ ps /\ ch) -> th)
2	1	3exp 611	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp32 281	1 |- ((ph /\ (ps /\ ch)) -> th)

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

This theorem is referenced by:  syl3an1 619  mp3an1 639  oaass 3163  nnmsucr 3182  add4t 4127  pncant 4161  npcant 4162  mul4t 4177  sup2 4510  zltp1let 4597  peano2uz 4602  flgzt 4626  qbtwnre 4650  hvadd4t 5013  hvsubcan1t 5016  shscl 5282  shmods 5363  spanunsn 5482  5oalem1 5544  3oalem2 5553

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