Theorem 3impb 1200

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

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

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 981

This theorem is referenced by:  3adant1l  1231  3adant1r  1232  3impdi  1303  vtocl3gf  2812  rspc2ev  2868  reuss  3428  trssord  4392  funtp  5281  resdif  5495  funimass4  5579  fnovex  5921  fnotovb  5931  fovcdm  6030  fnovrn  6035  fmpoco  6230  nndi  6500  nnaordi  6522  ecovass  6657  ecoviass  6658  ecovdi  6659  ecovidi  6660  eqsupti  7008  addasspig  7342  mulasspig  7344  distrpig  7345  distrnq0  7471  addassnq0  7474  distnq0r  7475  prcdnql  7496  prcunqu  7497  genpassl  7536  genpassu  7537  genpassg  7538  distrlem1prl  7594  distrlem1pru  7595  ltexprlemopl  7613  ltexprlemopu  7615  le2tri3i  8079  cnegexlem1  8145  subadd  8173  addsub  8181  subdi  8355  submul2  8369  div12ap  8664  diveqap1  8675  divnegap  8676  divdivap2  8694  ltmulgt11  8834  gt0div  8840  ge0div  8841  uzind3  9379  fnn0ind  9382  qdivcl  9656  irrmul  9660  xrlttr  9808  fzen  10056  lenegsq  11117  moddvds  11819  dvds2add  11845  dvds2sub  11846  dvdsleabs  11864  divalgb  11943  ndvdsadd  11949  modgcd  12005  absmulgcd  12031  odzval  12254  pcmul  12314  setsresg  12513  issubmnd  12864  submcl  12891  grpinvid1  12948  grpinvid2  12949  mulgp1  13047  cmncom  13138  islss3  13563  unopn  13776  innei  13934  cncfi  14336