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  6763  nnaordi  6785  ecovass  6922  ecoviass  6923  ecovdi  6924  ecovidi  6925  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  9770  fnn0ind  9773  qdivcl  10059  irrmul  10064  xrlttr  10214  fzen  10464  ccatval21sw  11395  lswccatn0lsw  11401  swrdwrdsymbg  11458  ccatpfx  11495  ccatopth  11510  lenegsq  11884  moddvds  12591  dvds2add  12617  dvds2sub  12618  dvdsleabs  12637  divalgb  12717  ndvdsadd  12723  modgcd  12793  absmulgcd  12819  odzval  13049  pcmul  13109  setsresg  13448  issubmnd  13814  submcl  13845  grpinvid1  13916  grpinvid2  13917  mulgp1  14017  ghmlin  14110  ghmsub  14113  cmncom  14195  prdssgrpd  14298  prdsmndd  14301  islss3  14825  unopn  15231  innei  15389  cncfi  15804