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  4527  funtp  5437  resdif  5664  funimass4  5756  fnovex  6121  fnotovb  6134  fovcdm  6235  fnovrn  6240  fmpoco  6456  nndi  6764  nnaordi  6786  ecovass  6923  ecoviass  6924  ecovdi  6925  ecovidi  6926  eqsupti  7342  addasspig  7703  mulasspig  7705  distrpig  7706  distrnq0  7832  addassnq0  7835  distnq0r  7836  prcdnql  7857  prcunqu  7858  genpassl  7897  genpassu  7898  genpassg  7899  distrlem1prl  7955  distrlem1pru  7956  ltexprlemopl  7974  ltexprlemopu  7976  le2tri3i  8441  cnegexlem1  8508  subadd  8536  addsub  8544  subdi  8719  submul2  8733  div12ap  9032  diveqap1  9043  divnegap  9044  divdivap2  9062  ltmulgt11  9202  gt0div  9208  ge0div  9209  uzind3  9769  fnn0ind  9772  qdivcl  10058  irrmul  10063  xrlttr  10213  fzen  10463  ccatval21sw  11394  lswccatn0lsw  11400  swrdwrdsymbg  11457  ccatpfx  11494  ccatopth  11509  lenegsq  11883  moddvds  12590  dvds2add  12616  dvds2sub  12617  dvdsleabs  12636  divalgb  12716  ndvdsadd  12722  modgcd  12792  absmulgcd  12818  odzval  13048  pcmul  13108  setsresg  13447  issubmnd  13813  submcl  13844  grpinvid1  13915  grpinvid2  13916  mulgp1  14016  ghmlin  14109  ghmsub  14112  cmncom  14194  prdssgrpd  14297  prdsmndd  14300  islss3  14824  unopn  15248  innei  15406  cncfi  15821