Theorem 3impb 1225

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

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

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 1006

This theorem is referenced by:  3adant1l  1256  3adant1r  1257  3impdi  1329  vtocl3gf  2867  rspc2ev  2925  reuss  3488  trssord  4477  funtp  5383  resdif  5605  funimass4  5696  fnovex  6051  fnotovb  6064  fovcdm  6165  fnovrn  6170  fmpoco  6381  nndi  6654  nnaordi  6676  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  eqsupti  7195  addasspig  7550  mulasspig  7552  distrpig  7553  distrnq0  7679  addassnq0  7682  distnq0r  7683  prcdnql  7704  prcunqu  7705  genpassl  7744  genpassu  7745  genpassg  7746  distrlem1prl  7802  distrlem1pru  7803  ltexprlemopl  7821  ltexprlemopu  7823  le2tri3i  8288  cnegexlem1  8354  subadd  8382  addsub  8390  subdi  8564  submul2  8578  div12ap  8874  diveqap1  8885  divnegap  8886  divdivap2  8904  ltmulgt11  9044  gt0div  9050  ge0div  9051  uzind3  9593  fnn0ind  9596  qdivcl  9877  irrmul  9881  xrlttr  10030  fzen  10278  ccatval21sw  11183  lswccatn0lsw  11189  swrdwrdsymbg  11246  ccatpfx  11283  ccatopth  11298  lenegsq  11657  moddvds  12362  dvds2add  12388  dvds2sub  12389  dvdsleabs  12408  divalgb  12488  ndvdsadd  12494  modgcd  12564  absmulgcd  12590  odzval  12816  pcmul  12876  setsresg  13122  prdssgrpd  13500  issubmnd  13527  prdsmndd  13533  submcl  13564  grpinvid1  13637  grpinvid2  13638  mulgp1  13744  ghmlin  13837  ghmsub  13840  cmncom  13891  islss3  14396  unopn  14732  innei  14890  cncfi  15305