Theorem 3impb 1147

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 588	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	3imp 1145	1 |- ((ph /\ ps /\ ch) -> th)

Syntax hints:   -> wi 4   /\ wa 358   /\ w3a 934

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

This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936

This theorem is referenced by:  3adant1l  1174  3adant1r  1175  3impdi  1237  vtocl3gf  2918  rspc2ev  2964  reuss  3537  pw1equn  4332  pw1eqadj  4333  preaddccan2  4456  resdif  5307  fnopovb  5558  fovrn  5605  fnovrn  5608  mucass  6136  addccan2nc  6266  nchoicelem3  6292