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  2917  rspc2ev  2963  reuss  3536  pw1equn  4331  pw1eqadj  4332  preaddccan2  4455  resdif  5306  fnopovb  5557  fovrn  5604  fnovrn  5607  mucass  6135  addccan2nc  6265  nchoicelem3  6291