Theorem 3impb 1201

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

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

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 982

This theorem is referenced by:  3adant1l  1232  3adant1r  1233  3impdi  1304  vtocl3gf  2824  rspc2ev  2880  reuss  3441  trssord  4412  funtp  5308  resdif  5523  funimass4  5608  fnovex  5952  fnotovb  5962  fovcdm  6063  fnovrn  6068  fmpoco  6271  nndi  6541  nnaordi  6563  ecovass  6700  ecoviass  6701  ecovdi  6702  ecovidi  6703  eqsupti  7057  addasspig  7392  mulasspig  7394  distrpig  7395  distrnq0  7521  addassnq0  7524  distnq0r  7525  prcdnql  7546  prcunqu  7547  genpassl  7586  genpassu  7587  genpassg  7588  distrlem1prl  7644  distrlem1pru  7645  ltexprlemopl  7663  ltexprlemopu  7665  le2tri3i  8130  cnegexlem1  8196  subadd  8224  addsub  8232  subdi  8406  submul2  8420  div12ap  8715  diveqap1  8726  divnegap  8727  divdivap2  8745  ltmulgt11  8885  gt0div  8891  ge0div  8892  uzind3  9433  fnn0ind  9436  qdivcl  9711  irrmul  9715  xrlttr  9864  fzen  10112  lenegsq  11242  moddvds  11945  dvds2add  11971  dvds2sub  11972  dvdsleabs  11990  divalgb  12069  ndvdsadd  12075  modgcd  12131  absmulgcd  12157  odzval  12382  pcmul  12442  setsresg  12659  issubmnd  13026  submcl  13054  grpinvid1  13127  grpinvid2  13128  mulgp1  13228  ghmlin  13321  ghmsub  13324  cmncom  13375  islss3  13878  unopn  14184  innei  14342  cncfi  14757