Theorem 3impb 1111

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3impb.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
3impb	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impb

Step	Hyp	Ref	Expression
1		3impb.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1107	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  3adant3  1128  3impdi  1346  rsp2e  3308  vtocl3gf  3574  rspc2ev  3638  reuss  4287  frc  5524  trssord  6211  funtp  6414  resdif  6638  fnotovb  7209  fovrn  7321  fnovrn  7326  fmpoco  7793  smoord  8005  odi  8208  oeoa  8226  oeoe  8228  nndi  8252  ecopovtrn  8403  ecovass  8407  ecovdi  8408  suppr  8938  infpr  8970  harval2  9429  fin23lem31  9768  tskuni  10208  addasspi  10320  mulasspi  10322  distrpi  10323  mulcanenq  10385  genpass  10434  distrlem1pr  10450  prlem934  10458  ltapr  10470  le2tri3i  10773  subadd  10892  addsub  10900  subdi  11076  submul2  11083  ltaddsub  11117  leaddsub  11119  divval  11303  div12  11323  diveq1  11334  divneg  11335  divdiv2  11355  ltmulgt11  11503  gt0div  11509  ge0div  11510  uzind3  12079  fnn0ind  12084  qdivcl  12372  irrmul  12376  xrlttr  12536  fzen  12927  modcyc  13277  modcyc2  13278  rpexpmord  13535  faclbnd4lem4  13659  ccatval21sw  13942  lswccatn0lsw  13948  ccatpfx  14066  ccatopth  14081  cshweqdifid  14185  lenegsq  14683  moddvds  15621  dvdscmulr  15641  dvdsmulcr  15642  dvds2add  15646  dvds2sub  15647  dvdsleabs  15664  divalg  15757  divalgb  15758  ndvdsadd  15764  gcdcllem3  15853  dvdslegcd  15856  modgcd  15883  absmulgcd  15900  odzval  16131  pcmul  16191  ressid2  16555  ressval2  16556  catcisolem  17369  prf1st  17457  prf2nd  17458  1st2ndprf  17459  curfuncf  17491  curf2ndf  17500  pltval  17573  pospo  17586  lubel  17735  isdlat  17806  issubmnd  17941  prdsmndd  17947  submcl  17980  grpinvid1  18157  grpinvid2  18158  mulgp1  18263  ghmlin  18366  ghmsub  18369  odlem2  18670  gexlem2  18710  lsmvalx  18767  efgtval  18852  cmncom  18926  lssvnegcl  19731  islss3  19734  prdslmodd  19744  evlslem2  20295  evlseu  20299  zntoslem  20706  maducoeval2  21252  madutpos  21254  madugsum  21255  madurid  21256  m2cpminvid  21364  pm2mpghm  21427  unopn  21514  ntrss  21666  innei  21736  t1sep2  21980  metustsym  23168  cncfi  23505  rrxds  23999  quotval  24884  abelthlem2  25023  mudivsum  26109  padicabv  26209  axsegconlem1  26706  nsnlplig  28261  nsnlpligALT  28262  grpoinvid1  28308  grpoinvid2  28309  grpodivval  28315  ablo4  28330  ablonncan  28336  nvnpcan  28436  nvmeq0  28438  nvabs  28452  imsdval  28466  ipval  28483  nmorepnf  28548  blo3i  28582  blometi  28583  ipasslem5  28615  hvmulcan  28852  his5  28866  his7  28870  his2sub2  28873  hhssabloilem  29041  hhssnv  29044  fh1  29398  fh2  29399  cm2j  29400  homcl  29526  homco1  29581  homulass  29582  hoadddi  29583  hosubsub2  29592  braadd  29725  bramul  29726  lnopmul  29747  lnopli  29748  lnopaddmuli  29753  lnopsubmuli  29755  lnfnli  29820  lnfnaddmuli  29825  kbass2  29897  mdexchi  30115  xdivval  30599  resvid2  30905  resvval2  30906  fedgmullem2  31030  unitdivcld  31148  bnj229  32160  bnj546  32172  bnj570  32181  cusgredgex2  32373  loop1cycl  32388  cvmlift2lem7  32560  nosupfv  33210  nosupres  33211  finminlem  33670  ivthALT  33687  topdifinffinlem  34632  lindsadd  34889  exidcl  35158  grposnOLD  35164  rngoneglmul  35225  rngonegrmul  35226  divrngcl  35239  crngocom  35283  crngm4  35285  inidl  35312  xrninxpex  35646  oposlem  36322  hlsuprexch  36521  ldilcnv  37255  ltrnu  37261  tgrpgrplem  37889  tgrpabl  37891  erngdvlem3  38130  erngdvlem3-rN  38138  dvalveclem  38165  dvhfvadd  38231  dvhgrp  38247  dvhlveclem  38248  djhval2  38539  resubadd  39215  diophren  39416  monotoddzzfi  39545  ltrmynn0  39551  ltrmxnn0  39552  lermxnn0  39553  rmyeq  39557  lermy  39558  jm2.21  39597  radcnvrat  40652  dvconstbi  40672  expgrowth  40673  bi3impb  40823  eel132  41042  xlimmnfvlem2  42120  xlimpnfvlem2  42124  fnotaovb  43404  submgmcl  44068  onetansqsecsq  44867