Theorem 3impb 1140

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

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 925

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

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  3adant1l  1167  3adant1r  1168  3impdi  1230  vtocl3gf  2683  rspc2ev  2737  reuss  3281  trssord  4216  funtp  5080  resdif  5288  funimass4  5368  fnovex  5696  fnotovb  5706  fovrn  5801  fnovrn  5806  fmpt2co  5995  nndi  6261  nnaordi  6281  ecovass  6415  ecoviass  6416  ecovdi  6417  ecovidi  6418  eqsupti  6745  addasspig  6950  mulasspig  6952  distrpig  6953  distrnq0  7079  addassnq0  7082  distnq0r  7083  prcdnql  7104  prcunqu  7105  genpassl  7144  genpassu  7145  genpassg  7146  distrlem1prl  7202  distrlem1pru  7203  ltexprlemopl  7221  ltexprlemopu  7223  le2tri3i  7654  cnegexlem1  7718  subadd  7746  addsub  7754  subdi  7924  submul2  7938  div12ap  8222  diveqap1  8233  divnegap  8234  divdivap2  8252  ltmulgt11  8386  gt0div  8392  ge0div  8393  uzind3  8920  fnn0ind  8923  qdivcl  9189  irrmul  9193  xrlttr  9326  fzen  9518  iseqval  9932  lenegsq  10589  moddvds  11144  dvds2add  11169  dvds2sub  11170  dvdsleabs  11185  divalgb  11264  ndvdsadd  11270  modgcd  11321  absmulgcd  11345  setsresg  11593  unopn  11765  cncfi  11907