Theorem 3impb 1194

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

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

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

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

This theorem is referenced by:  3adant1l  1225  3adant1r  1226  3impdi  1288  vtocl3gf  2793  rspc2ev  2849  reuss  3408  trssord  4365  funtp  5251  resdif  5464  funimass4  5547  fnovex  5886  fnotovb  5896  fovrn  5995  fnovrn  6000  fmpoco  6195  nndi  6465  nnaordi  6487  ecovass  6622  ecoviass  6623  ecovdi  6624  ecovidi  6625  eqsupti  6973  addasspig  7292  mulasspig  7294  distrpig  7295  distrnq0  7421  addassnq0  7424  distnq0r  7425  prcdnql  7446  prcunqu  7447  genpassl  7486  genpassu  7487  genpassg  7488  distrlem1prl  7544  distrlem1pru  7545  ltexprlemopl  7563  ltexprlemopu  7565  le2tri3i  8028  cnegexlem1  8094  subadd  8122  addsub  8130  subdi  8304  submul2  8318  div12ap  8611  diveqap1  8622  divnegap  8623  divdivap2  8641  ltmulgt11  8780  gt0div  8786  ge0div  8787  uzind3  9325  fnn0ind  9328  qdivcl  9602  irrmul  9606  xrlttr  9752  fzen  9999  lenegsq  11059  moddvds  11761  dvds2add  11787  dvds2sub  11788  dvdsleabs  11805  divalgb  11884  ndvdsadd  11890  modgcd  11946  absmulgcd  11972  odzval  12195  pcmul  12255  setsresg  12454  submcl  12701  grpinvid1  12754  grpinvid2  12755  unopn  12797  innei  12957  cncfi  13359