Theorem 3impb 1134

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

Syntax hints:   -> wi 4   /\ wa 102   /\ w3a 919

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  3adant1l  1161  3adant1r  1162  3impdi  1224  vtocl3gf  2661  rspc2ev  2715  reuss  3245  trssord  4135  funtp  4972  resdif  5168  funimass4  5245  fnovex  5558  fnotovb  5568  fovrn  5663  fnovrn  5668  fmpt2co  5857  nndi  6088  nnaordi  6104  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  eqsupti  6409  addasspig  6520  mulasspig  6522  distrpig  6523  distrnq0  6649  addassnq0  6652  distnq0r  6653  prcdnql  6674  prcunqu  6675  genpassl  6714  genpassu  6715  genpassg  6716  distrlem1prl  6772  distrlem1pru  6773  ltexprlemopl  6791  ltexprlemopu  6793  le2tri3i  7219  cnegexlem1  7283  subadd  7311  addsub  7319  subdi  7489  submul2  7503  div12ap  7782  diveqap1  7793  divnegap  7794  divdivap2  7812  ltmulgt11  7942  gt0div  7948  ge0div  7949  uzind3  8460  fnn0ind  8463  qdivcl  8728  irrmul  8732  xrlttr  8870  fzen  9062  iseqval  9440  lenegsq  9981  moddvds  10204  dvds2add  10229  dvds2sub  10230  dvdsleabs  10245  divalgb  10325  ndvdsadd  10331  modgcd  10382  absmulgcd  10406