Theorem 3impb 1116

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  3adant3  1133  3impdi  1351  rsp2e  3214  vtocl3gf  3474  rspc2ev  3536  reuss  4202  frc  5485  trssord  6183  funtp  6390  resdif  6632  f1ofvswap  7067  fnotovb  7214  fovrn  7328  fnovrn  7333  fmpoco  7809  smoord  8024  odi  8229  oeoa  8247  oeoe  8249  nndi  8273  ecopovtrn  8424  ecovass  8428  ecovdi  8429  unfi  8764  entrfil  8776  suppr  9001  infpr  9033  harval2  9492  fin23lem31  9836  tskuni  10276  addasspi  10388  mulasspi  10390  distrpi  10391  mulcanenq  10453  genpass  10502  distrlem1pr  10518  prlem934  10526  ltapr  10538  le2tri3i  10841  subadd  10960  addsub  10968  subdi  11144  submul2  11151  ltaddsub  11185  leaddsub  11187  divval  11371  div12  11391  diveq1  11402  divneg  11403  divdiv2  11423  ltmulgt11  11571  gt0div  11577  ge0div  11578  uzind3  12150  fnn0ind  12155  qdivcl  12445  irrmul  12449  xrlttr  12609  fzen  13008  modcyc  13358  modcyc2  13359  rpexpmord  13617  faclbnd4lem4  13741  ccatval21sw  14021  lswccatn0lsw  14027  ccatpfx  14145  ccatopth  14160  cshweqdifid  14264  lenegsq  14763  moddvds  15703  dvdscmulr  15723  dvdsmulcr  15724  dvds2add  15728  dvds2sub  15729  dvdsleabs  15749  divalg  15841  divalgb  15842  ndvdsadd  15848  gcdcllem3  15937  dvdslegcd  15940  modgcd  15969  absmulgcd  15986  odzval  16221  pcmul  16281  ressid2  16648  ressval2  16649  catcisolem  17475  prf1st  17563  prf2nd  17564  1st2ndprf  17565  curfuncf  17597  curf2ndf  17606  pltval  17679  pospo  17692  lubel  17841  isdlat  17912  issubmnd  18047  prdsmndd  18053  submcl  18086  grpinvid1  18265  grpinvid2  18266  mulgp1  18371  ghmlin  18474  ghmsub  18477  odlem2  18778  gexlem2  18818  lsmvalx  18875  efgtval  18960  cmncom  19034  lssvnegcl  19840  islss3  19843  prdslmodd  19853  zntoslem  20368  evlslem2  20886  evlseu  20890  maducoeval2  21384  madutpos  21386  madugsum  21387  madurid  21388  m2cpminvid  21497  pm2mpghm  21560  unopn  21647  ntrss  21799  innei  21869  t1sep2  22113  metustsym  23301  cncfi  23639  rrxds  24138  quotval  25032  abelthlem2  25171  mudivsum  26258  padicabv  26358  axsegconlem1  26855  nsnlplig  28408  nsnlpligALT  28409  grpoinvid1  28455  grpoinvid2  28456  grpodivval  28462  ablo4  28477  ablonncan  28483  nvnpcan  28583  nvmeq0  28585  nvabs  28599  imsdval  28613  ipval  28630  nmorepnf  28695  blo3i  28729  blometi  28730  ipasslem5  28762  hvmulcan  28999  his5  29013  his7  29017  his2sub2  29020  hhssabloilem  29188  hhssnv  29191  fh1  29545  fh2  29546  cm2j  29547  homcl  29673  homco1  29728  homulass  29729  hoadddi  29730  hosubsub2  29739  braadd  29872  bramul  29873  lnopmul  29894  lnopli  29895  lnopaddmuli  29900  lnopsubmuli  29902  lnfnli  29967  lnfnaddmuli  29972  kbass2  30044  mdexchi  30262  xdivval  30760  resvid2  31096  resvval2  31097  fedgmullem2  31275  unitdivcld  31415  bnj229  32427  bnj546  32439  bnj570  32448  cusgredgex2  32647  loop1cycl  32662  cvmlift2lem7  32834  nosupfv  33542  nosupres  33543  noinffv  33557  ssltsepc  33620  finminlem  34137  ivthALT  34154  topdifinffinlem  35130  lindsadd  35382  exidcl  35646  grposnOLD  35652  rngoneglmul  35713  rngonegrmul  35714  divrngcl  35727  crngocom  35771  crngm4  35773  inidl  35800  xrninxpex  36132  oposlem  36808  hlsuprexch  37007  ldilcnv  37741  ltrnu  37747  tgrpgrplem  38375  tgrpabl  38377  erngdvlem3  38616  erngdvlem3-rN  38624  dvalveclem  38651  dvhfvadd  38717  dvhgrp  38733  dvhlveclem  38734  djhval2  39025  resubadd  39923  diophren  40191  monotoddzzfi  40320  ltrmynn0  40326  ltrmxnn0  40327  lermxnn0  40328  rmyeq  40332  lermy  40333  jm2.21  40372  radcnvrat  41454  dvconstbi  41474  expgrowth  41475  bi3impb  41625  eel132  41844  xlimmnfvlem2  42900  xlimpnfvlem2  42904  fnotaovb  44207  submgmcl  44866  onetansqsecsq  45900