Theorem 3impb 1178

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 363	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	3imp 1176	1 |- ( ( ph /\ ps /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  3adant1l  1209  3adant1r  1210  3impdi  1272  vtocl3gf  2752  rspc2ev  2808  reuss  3362  trssord  4310  funtp  5184  resdif  5397  funimass4  5480  fnovex  5812  fnotovb  5822  fovrn  5921  fnovrn  5926  fmpoco  6121  nndi  6390  nnaordi  6412  ecovass  6546  ecoviass  6547  ecovdi  6548  ecovidi  6549  eqsupti  6891  addasspig  7162  mulasspig  7164  distrpig  7165  distrnq0  7291  addassnq0  7294  distnq0r  7295  prcdnql  7316  prcunqu  7317  genpassl  7356  genpassu  7357  genpassg  7358  distrlem1prl  7414  distrlem1pru  7415  ltexprlemopl  7433  ltexprlemopu  7435  le2tri3i  7896  cnegexlem1  7961  subadd  7989  addsub  7997  subdi  8171  submul2  8185  div12ap  8478  diveqap1  8489  divnegap  8490  divdivap2  8508  ltmulgt11  8646  gt0div  8652  ge0div  8653  uzind3  9188  fnn0ind  9191  qdivcl  9462  irrmul  9466  xrlttr  9611  fzen  9854  lenegsq  10899  moddvds  11538  dvds2add  11563  dvds2sub  11564  dvdsleabs  11579  divalgb  11658  ndvdsadd  11664  modgcd  11715  absmulgcd  11741  setsresg  12036  unopn  12211  innei  12371  cncfi  12773