Theorem 3impb 1115

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 420	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1111	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3adant3  1133  syl3an132  1167  3impdi  1352  rsp2e  3255  vtocl3gf  3516  vtocl3g  3518  rspc2ev  3577  reuss  4267  frc  5594  trssord  6340  funtp  6555  resdif  6801  f1cdmsn  7237  f1ofvswap  7261  fnotovb  7419  fovcdm  7537  fnovrn  7542  fmpoco  8045  smoord  8305  odi  8514  oeoa  8533  oeoe  8535  nndi  8559  ecopovtrn  8767  ecovass  8771  ecovdi  8772  unfi  9105  entrfil  9119  domtrfil  9126  f1imaenfi  9129  suppr  9385  infpr  9418  harval2  9921  fin23lem31  10265  tskuni  10706  addasspi  10818  mulasspi  10820  distrpi  10821  mulcanenq  10883  genpass  10932  distrlem1pr  10948  prlem934  10956  ltapr  10968  le2tri3i  11276  subadd  11396  addsub  11404  subdi  11583  submul2  11590  ltaddsub  11624  leaddsub  11626  divval  11811  diveq0  11819  div12  11831  diveq1  11839  divneg  11846  divdiv2  11867  ltmulgt11  12015  gt0div  12022  ge0div  12023  uzind3  12623  fnn0ind  12628  qdivcl  12920  irrmul  12924  xrlttr  13091  fzen  13495  modcyc  13865  modcyc2  13866  rpexpmord  14130  faclbnd4lem4  14258  ccatval21sw  14548  lswccatn0lsw  14554  ccatpfx  14663  ccatopth  14678  cshweqdifid  14782  lenegsq  15283  moddvds  16232  dvdscmulr  16253  dvdsmulcr  16254  dvds2add  16259  dvds2sub  16260  dvdsleabs  16280  divalg  16372  divalgb  16373  ndvdsadd  16379  gcdcllem3  16470  dvdslegcd  16473  modgcd  16501  absmulgcd  16518  odzval  16762  pcmul  16822  ressid2  17204  ressval2  17205  catcisolem  18077  prf1st  18170  prf2nd  18171  1st2ndprf  18172  curfuncf  18204  curf2ndf  18213  pltval  18296  pospo  18309  lubel  18480  isdlat  18488  submgmcl  18675  prdssgrpd  18701  issubmnd  18729  prdsmndd  18738  submcl  18780  grpinvid1  18967  grpinvid2  18968  mulgp1  19083  ghmlin  19196  ghmsub  19199  odlem2  19514  gexlem2  19557  lsmvalx  19614  efgtval  19698  cmncom  19773  lssvnegcl  20951  islss3  20954  prdslmodd  20964  zntoslem  21536  evlslem2  22057  evlseu  22061  maducoeval2  22605  madutpos  22607  madugsum  22608  madurid  22609  m2cpminvid  22718  pm2mpghm  22781  unopn  22868  ntrss  23020  innei  23090  t1sep2  23334  metustsym  24520  cncfi  24861  rrxds  25360  quotval  26258  abelthlem2  26397  mudivsum  27493  padicabv  27593  nosupfv  27670  nosupres  27671  noinffv  27685  sltssepc  27763  divsval  28181  axsegconlem1  28986  nsnlplig  30552  nsnlpligALT  30553  grpoinvid1  30599  grpoinvid2  30600  grpodivval  30606  ablo4  30621  ablonncan  30627  nvnpcan  30727  nvmeq0  30729  nvabs  30743  imsdval  30757  ipval  30774  nmorepnf  30839  blo3i  30873  blometi  30874  ipasslem5  30906  hvmulcan  31143  his5  31157  his7  31161  his2sub2  31164  hhssabloilem  31332  hhssnv  31335  fh1  31689  fh2  31690  cm2j  31691  homcl  31817  homco1  31872  homulass  31873  hoadddi  31874  hosubsub2  31883  braadd  32016  bramul  32017  lnopmul  32038  lnopli  32039  lnopaddmuli  32044  lnopsubmuli  32046  lnfnli  32111  lnfnaddmuli  32116  kbass2  32188  mdexchi  32406  xdivval  32978  resvid2  33390  resvval2  33391  fedgmullem2  33774  unitdivcld  34045  bnj229  35026  bnj546  35038  bnj570  35047  rankfilimb  35245  cusgredgex2  35305  loop1cycl  35319  cvmlift2lem7  35491  finminlem  36500  ivthALT  36517  topdifinffinlem  37663  lindsadd  37934  exidcl  38197  grposnOLD  38203  rngoneglmul  38264  rngonegrmul  38265  divrngcl  38278  crngocom  38322  crngm4  38324  inidl  38351  xrninxpex  38738  oposlem  39628  hlsuprexch  39827  ldilcnv  40561  ltrnu  40567  tgrpgrplem  41195  tgrpabl  41197  erngdvlem3  41436  erngdvlem3-rN  41444  dvalveclem  41471  dvhfvadd  41537  dvhgrp  41553  dvhlveclem  41554  djhval2  41845  f1o2d2  42674  fmpocos  42675  resubadd  42811  diophren  43241  monotoddzzfi  43370  ltrmynn0  43376  ltrmxnn0  43377  lermxnn0  43378  rmyeq  43382  lermy  43383  jm2.21  43422  radcnvrat  44741  dvconstbi  44761  expgrowth  44762  bi3impb  44911  xlimmnfvlem2  46261  xlimpnfvlem2  46265  fnotaovb  47646  tposcurf1  49774  precofvalALT  49843  onetansqsecsq  50236