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  3445  trssord  4416  funtp  5312  resdif  5529  funimass4  5614  fnovex  5958  fnotovb  5969  fovcdm  6070  fnovrn  6075  fmpoco  6283  nndi  6553  nnaordi  6575  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  eqsupti  7071  addasspig  7414  mulasspig  7416  distrpig  7417  distrnq0  7543  addassnq0  7546  distnq0r  7547  prcdnql  7568  prcunqu  7569  genpassl  7608  genpassu  7609  genpassg  7610  distrlem1prl  7666  distrlem1pru  7667  ltexprlemopl  7685  ltexprlemopu  7687  le2tri3i  8152  cnegexlem1  8218  subadd  8246  addsub  8254  subdi  8428  submul2  8442  div12ap  8738  diveqap1  8749  divnegap  8750  divdivap2  8768  ltmulgt11  8908  gt0div  8914  ge0div  8915  uzind3  9456  fnn0ind  9459  qdivcl  9734  irrmul  9738  xrlttr  9887  fzen  10135  lenegsq  11277  moddvds  11981  dvds2add  12007  dvds2sub  12008  dvdsleabs  12027  divalgb  12107  ndvdsadd  12113  modgcd  12183  absmulgcd  12209  odzval  12435  pcmul  12495  setsresg  12741  prdssgrpd  13117  issubmnd  13144  prdsmndd  13150  submcl  13181  grpinvid1  13254  grpinvid2  13255  mulgp1  13361  ghmlin  13454  ghmsub  13457  cmncom  13508  islss3  14011  unopn  14325  innei  14483  cncfi  14898