Theorem 3impb 1202

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

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

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 983

This theorem is referenced by:  3adant1l  1233  3adant1r  1234  3impdi  1306  vtocl3gf  2836  rspc2ev  2892  reuss  3454  trssord  4427  funtp  5327  resdif  5544  funimass4  5629  fnovex  5977  fnotovb  5988  fovcdm  6089  fnovrn  6094  fmpoco  6302  nndi  6572  nnaordi  6594  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  eqsupti  7098  addasspig  7443  mulasspig  7445  distrpig  7446  distrnq0  7572  addassnq0  7575  distnq0r  7576  prcdnql  7597  prcunqu  7598  genpassl  7637  genpassu  7638  genpassg  7639  distrlem1prl  7695  distrlem1pru  7696  ltexprlemopl  7714  ltexprlemopu  7716  le2tri3i  8181  cnegexlem1  8247  subadd  8275  addsub  8283  subdi  8457  submul2  8471  div12ap  8767  diveqap1  8778  divnegap  8779  divdivap2  8797  ltmulgt11  8937  gt0div  8943  ge0div  8944  uzind3  9486  fnn0ind  9489  qdivcl  9764  irrmul  9768  xrlttr  9917  fzen  10165  ccatval21sw  11061  lswccatn0lsw  11067  swrdwrdsymbg  11117  lenegsq  11406  moddvds  12110  dvds2add  12136  dvds2sub  12137  dvdsleabs  12156  divalgb  12236  ndvdsadd  12242  modgcd  12312  absmulgcd  12338  odzval  12564  pcmul  12624  setsresg  12870  prdssgrpd  13247  issubmnd  13274  prdsmndd  13280  submcl  13311  grpinvid1  13384  grpinvid2  13385  mulgp1  13491  ghmlin  13584  ghmsub  13587  cmncom  13638  islss3  14141  unopn  14477  innei  14635  cncfi  15050