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  5594  funimass4  5684  fnovex  6034  fnotovb  6047  fovcdm  6148  fnovrn  6153  fmpoco  6362  nndi  6632  nnaordi  6654  ecovass  6791  ecoviass  6792  ecovdi  6793  ecovidi  6794  eqsupti  7163  addasspig  7517  mulasspig  7519  distrpig  7520  distrnq0  7646  addassnq0  7649  distnq0r  7650  prcdnql  7671  prcunqu  7672  genpassl  7711  genpassu  7712  genpassg  7713  distrlem1prl  7769  distrlem1pru  7770  ltexprlemopl  7788  ltexprlemopu  7790  le2tri3i  8255  cnegexlem1  8321  subadd  8349  addsub  8357  subdi  8531  submul2  8545  div12ap  8841  diveqap1  8852  divnegap  8853  divdivap2  8871  ltmulgt11  9011  gt0div  9017  ge0div  9018  uzind3  9560  fnn0ind  9563  qdivcl  9838  irrmul  9842  xrlttr  9991  fzen  10239  ccatval21sw  11140  lswccatn0lsw  11146  swrdwrdsymbg  11196  ccatpfx  11233  ccatopth  11248  lenegsq  11606  moddvds  12310  dvds2add  12336  dvds2sub  12337  dvdsleabs  12356  divalgb  12436  ndvdsadd  12442  modgcd  12512  absmulgcd  12538  odzval  12764  pcmul  12824  setsresg  13070  prdssgrpd  13448  issubmnd  13475  prdsmndd  13481  submcl  13512  grpinvid1  13585  grpinvid2  13586  mulgp1  13692  ghmlin  13785  ghmsub  13788  cmncom  13839  islss3  14343  unopn  14679  innei  14837  cncfi  15252