Theorem 3impb 1177

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

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

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 964

This theorem is referenced by:  3adant1l  1208  3adant1r  1209  3impdi  1271  vtocl3gf  2744  rspc2ev  2799  reuss  3352  trssord  4297  funtp  5171  resdif  5382  funimass4  5465  fnovex  5797  fnotovb  5807  fovrn  5906  fnovrn  5911  fmpoco  6106  nndi  6375  nnaordi  6397  ecovass  6531  ecoviass  6532  ecovdi  6533  ecovidi  6534  eqsupti  6876  addasspig  7131  mulasspig  7133  distrpig  7134  distrnq0  7260  addassnq0  7263  distnq0r  7264  prcdnql  7285  prcunqu  7286  genpassl  7325  genpassu  7326  genpassg  7327  distrlem1prl  7383  distrlem1pru  7384  ltexprlemopl  7402  ltexprlemopu  7404  le2tri3i  7865  cnegexlem1  7930  subadd  7958  addsub  7966  subdi  8140  submul2  8154  div12ap  8447  diveqap1  8458  divnegap  8459  divdivap2  8477  ltmulgt11  8615  gt0div  8621  ge0div  8622  uzind3  9157  fnn0ind  9160  qdivcl  9428  irrmul  9432  xrlttr  9574  fzen  9816  lenegsq  10860  moddvds  11491  dvds2add  11516  dvds2sub  11517  dvdsleabs  11532  divalgb  11611  ndvdsadd  11617  modgcd  11668  absmulgcd  11694  setsresg  11986  unopn  12161  innei  12321  cncfi  12723