Theorem 3impb 1230

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3adant1l  1261  3adant1r  1262  3impdi  1334  vtocl3gf  2886  rspc2ev  2945  reuss  3514  trssord  4525  funtp  5434  resdif  5661  funimass4  5753  fnovex  6118  fnotovb  6131  fovcdm  6232  fnovrn  6237  fmpoco  6452  nndi  6759  nnaordi  6781  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  eqsupti  7337  addasspig  7698  mulasspig  7700  distrpig  7701  distrnq0  7827  addassnq0  7830  distnq0r  7831  prcdnql  7852  prcunqu  7853  genpassl  7892  genpassu  7893  genpassg  7894  distrlem1prl  7950  distrlem1pru  7951  ltexprlemopl  7969  ltexprlemopu  7971  le2tri3i  8436  cnegexlem1  8503  subadd  8531  addsub  8539  subdi  8714  submul2  8728  div12ap  9027  diveqap1  9038  divnegap  9039  divdivap2  9057  ltmulgt11  9197  gt0div  9203  ge0div  9204  uzind3  9764  fnn0ind  9767  qdivcl  10053  irrmul  10058  xrlttr  10208  fzen  10458  ccatval21sw  11389  lswccatn0lsw  11395  swrdwrdsymbg  11452  ccatpfx  11489  ccatopth  11504  lenegsq  11878  moddvds  12585  dvds2add  12611  dvds2sub  12612  dvdsleabs  12631  divalgb  12711  ndvdsadd  12717  modgcd  12787  absmulgcd  12813  odzval  13043  pcmul  13103  setsresg  13442  issubmnd  13808  submcl  13839  grpinvid1  13910  grpinvid2  13911  mulgp1  14011  ghmlin  14104  ghmsub  14107  cmncom  14189  prdssgrpd  14275  prdsmndd  14278  islss3  14800  unopn  15197  innei  15355  cncfi  15770