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  2827  rspc2ev  2883  reuss  3444  trssord  4415  funtp  5311  resdif  5526  funimass4  5611  fnovex  5955  fnotovb  5965  fovcdm  6066  fnovrn  6071  fmpoco  6274  nndi  6544  nnaordi  6566  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  eqsupti  7062  addasspig  7397  mulasspig  7399  distrpig  7400  distrnq0  7526  addassnq0  7529  distnq0r  7530  prcdnql  7551  prcunqu  7552  genpassl  7591  genpassu  7592  genpassg  7593  distrlem1prl  7649  distrlem1pru  7650  ltexprlemopl  7668  ltexprlemopu  7670  le2tri3i  8135  cnegexlem1  8201  subadd  8229  addsub  8237  subdi  8411  submul2  8425  div12ap  8721  diveqap1  8732  divnegap  8733  divdivap2  8751  ltmulgt11  8891  gt0div  8897  ge0div  8898  uzind3  9439  fnn0ind  9442  qdivcl  9717  irrmul  9721  xrlttr  9870  fzen  10118  lenegsq  11260  moddvds  11964  dvds2add  11990  dvds2sub  11991  dvdsleabs  12010  divalgb  12090  ndvdsadd  12096  modgcd  12158  absmulgcd  12184  odzval  12410  pcmul  12470  setsresg  12716  issubmnd  13083  submcl  13111  grpinvid1  13184  grpinvid2  13185  mulgp1  13285  ghmlin  13378  ghmsub  13381  cmncom  13432  islss3  13935  unopn  14241  innei  14399  cncfi  14814