Theorem 3impib 1227

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
2	1	expd 258	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1219	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104   /\ w3a 1004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1006

This theorem is referenced by:  mob  2988  eqreu  2998  iotam  5318  funimaexglem  5413  ssimaexg  5708  funopdmsn  5834  rbropap  6409  dfsmo2  6453  3ecoptocl  6793  distrnq0  7679  addassnq0  7682  uzind  9591  fzind  9595  fnn0ind  9596  xltnegi  10070  facwordi  11003  shftvalg  11414  shftval4g  11415  mulgcd  12605  coprmdvds1  12681  pcfac  12941  mgmcl  13460  mhmlin  13568  mhmmulg  13768  issubg2m  13794  nsgbi  13809  srgmulgass  14021  dvdsrtr  14134  issubrng2  14243  issubrg2  14274  domnmuln0  14306  inopn  14746  basis1  14790  cnmpt2t  15036  cnmpt22  15037  cnmptcom  15041  xmeteq0  15102  sincosq1sgn  15569  sincosq2sgn  15570  sincosq3sgn  15571  sincosq4sgn  15572  speano5  16590