Theorem 3impb 1181

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

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

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 965

This theorem is referenced by:  3adant1l  1212  3adant1r  1213  3impdi  1275  vtocl3gf  2775  rspc2ev  2831  reuss  3388  trssord  4340  funtp  5223  resdif  5436  funimass4  5519  fnovex  5854  fnotovb  5864  fovrn  5963  fnovrn  5968  fmpoco  6163  nndi  6433  nnaordi  6455  ecovass  6589  ecoviass  6590  ecovdi  6591  ecovidi  6592  eqsupti  6940  addasspig  7250  mulasspig  7252  distrpig  7253  distrnq0  7379  addassnq0  7382  distnq0r  7383  prcdnql  7404  prcunqu  7405  genpassl  7444  genpassu  7445  genpassg  7446  distrlem1prl  7502  distrlem1pru  7503  ltexprlemopl  7521  ltexprlemopu  7523  le2tri3i  7985  cnegexlem1  8050  subadd  8078  addsub  8086  subdi  8260  submul2  8274  div12ap  8567  diveqap1  8578  divnegap  8579  divdivap2  8597  ltmulgt11  8735  gt0div  8741  ge0div  8742  uzind3  9277  fnn0ind  9280  qdivcl  9552  irrmul  9556  xrlttr  9702  fzen  9945  lenegsq  10995  moddvds  11695  dvds2add  11720  dvds2sub  11721  dvdsleabs  11736  divalgb  11815  ndvdsadd  11821  modgcd  11874  absmulgcd  11900  odzval  12115  setsresg  12228  unopn  12403  innei  12563  cncfi  12965