Theorem 3impb 1189

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 1183	1 |- ( ( ph /\ ps /\ ch ) -> th )

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

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 970

This theorem is referenced by:  3adant1l  1220  3adant1r  1221  3impdi  1283  vtocl3gf  2788  rspc2ev  2844  reuss  3402  trssord  4357  funtp  5240  resdif  5453  funimass4  5536  fnovex  5871  fnotovb  5881  fovrn  5980  fnovrn  5985  fmpoco  6180  nndi  6450  nnaordi  6472  ecovass  6606  ecoviass  6607  ecovdi  6608  ecovidi  6609  eqsupti  6957  addasspig  7267  mulasspig  7269  distrpig  7270  distrnq0  7396  addassnq0  7399  distnq0r  7400  prcdnql  7421  prcunqu  7422  genpassl  7461  genpassu  7462  genpassg  7463  distrlem1prl  7519  distrlem1pru  7520  ltexprlemopl  7538  ltexprlemopu  7540  le2tri3i  8003  cnegexlem1  8069  subadd  8097  addsub  8105  subdi  8279  submul2  8293  div12ap  8586  diveqap1  8597  divnegap  8598  divdivap2  8616  ltmulgt11  8755  gt0div  8761  ge0div  8762  uzind3  9300  fnn0ind  9303  qdivcl  9577  irrmul  9581  xrlttr  9727  fzen  9974  lenegsq  11033  moddvds  11735  dvds2add  11761  dvds2sub  11762  dvdsleabs  11779  divalgb  11858  ndvdsadd  11864  modgcd  11920  absmulgcd  11946  odzval  12169  pcmul  12229  setsresg  12428  unopn  12603  innei  12763  cncfi  13165