Theorem 3impb 1226

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

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

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 1007

This theorem is referenced by:  3adant1l  1257  3adant1r  1258  3impdi  1330  vtocl3gf  2868  rspc2ev  2926  reuss  3490  trssord  4483  funtp  5390  resdif  5614  funimass4  5705  fnovex  6061  fnotovb  6074  fovcdm  6175  fnovrn  6180  fmpoco  6390  nndi  6697  nnaordi  6719  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  eqsupti  7255  addasspig  7610  mulasspig  7612  distrpig  7613  distrnq0  7739  addassnq0  7742  distnq0r  7743  prcdnql  7764  prcunqu  7765  genpassl  7804  genpassu  7805  genpassg  7806  distrlem1prl  7862  distrlem1pru  7863  ltexprlemopl  7881  ltexprlemopu  7883  le2tri3i  8347  cnegexlem1  8413  subadd  8441  addsub  8449  subdi  8623  submul2  8637  div12ap  8933  diveqap1  8944  divnegap  8945  divdivap2  8963  ltmulgt11  9103  gt0div  9109  ge0div  9110  uzind3  9654  fnn0ind  9657  qdivcl  9938  irrmul  9942  xrlttr  10091  fzen  10340  ccatval21sw  11248  lswccatn0lsw  11254  swrdwrdsymbg  11311  ccatpfx  11348  ccatopth  11363  lenegsq  11735  moddvds  12440  dvds2add  12466  dvds2sub  12467  dvdsleabs  12486  divalgb  12566  ndvdsadd  12572  modgcd  12642  absmulgcd  12668  odzval  12894  pcmul  12954  setsresg  13200  prdssgrpd  13578  issubmnd  13605  prdsmndd  13611  submcl  13642  grpinvid1  13715  grpinvid2  13716  mulgp1  13822  ghmlin  13915  ghmsub  13918  cmncom  13969  islss3  14475  unopn  14816  innei  14974  cncfi  15389