Theorem 3impb 1223

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

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

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 1004

This theorem is referenced by:  3adant1l  1254  3adant1r  1255  3impdi  1327  vtocl3gf  2864  rspc2ev  2922  reuss  3485  trssord  4471  funtp  5374  resdif  5596  funimass4  5686  fnovex  6040  fnotovb  6053  fovcdm  6154  fnovrn  6159  fmpoco  6368  nndi  6640  nnaordi  6662  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  eqsupti  7174  addasspig  7528  mulasspig  7530  distrpig  7531  distrnq0  7657  addassnq0  7660  distnq0r  7661  prcdnql  7682  prcunqu  7683  genpassl  7722  genpassu  7723  genpassg  7724  distrlem1prl  7780  distrlem1pru  7781  ltexprlemopl  7799  ltexprlemopu  7801  le2tri3i  8266  cnegexlem1  8332  subadd  8360  addsub  8368  subdi  8542  submul2  8556  div12ap  8852  diveqap1  8863  divnegap  8864  divdivap2  8882  ltmulgt11  9022  gt0div  9028  ge0div  9029  uzind3  9571  fnn0ind  9574  qdivcl  9850  irrmul  9854  xrlttr  10003  fzen  10251  ccatval21sw  11153  lswccatn0lsw  11159  swrdwrdsymbg  11212  ccatpfx  11249  ccatopth  11264  lenegsq  11622  moddvds  12326  dvds2add  12352  dvds2sub  12353  dvdsleabs  12372  divalgb  12452  ndvdsadd  12458  modgcd  12528  absmulgcd  12554  odzval  12780  pcmul  12840  setsresg  13086  prdssgrpd  13464  issubmnd  13491  prdsmndd  13497  submcl  13528  grpinvid1  13601  grpinvid2  13602  mulgp1  13708  ghmlin  13801  ghmsub  13804  cmncom  13855  islss3  14359  unopn  14695  innei  14853  cncfi  15268