Theorem 3impb 1126

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 1122	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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

This theorem is referenced by:  3adant3  1144  syl3an132  1178  3impdi  1363  rsp2e  3279  vtocl3gf  3536  vtocl3g  3538  rspc2ev  3593  reuss  4277  frc  5606  trssord  6358  funtp  6573  resdif  6823  f1cdmsn  7261  f1ofvswap  7285  fnotovb  7443  fovcdm  7561  fnovrn  7566  fmpoco  8068  mpof1o2d  8099  smoord  8330  odi  8542  oeoa  8561  oeoe  8563  nndi  8587  ecopovtrn  8796  ecovass  8800  ecovdi  8801  unfi  9133  entrfil  9147  domtrfil  9154  f1imaenfi  9157  suppr  9412  infpr  9445  harval2  9949  fin23lem31  10294  tskuni  10735  addasspi  10847  mulasspi  10849  distrpi  10850  mulcanenq  10912  genpass  10961  distrlem1pr  10977  prlem934  10985  ltapr  10997  le2tri3i  11307  subadd  11427  addsub  11435  subdi  11614  submul2  11621  ltaddsub  11655  leaddsub  11657  divval  11841  diveq0  11849  div12  11861  diveq1  11869  divneg  11876  divdiv2  11897  ltmulgt11  12045  gt0div  12052  ge0div  12053  uzind3  12661  fnn0ind  12666  qdivcl  12965  irrmul  12969  xrlttr  13136  fzen  13540  modcyc  13910  modcyc2  13911  rpexpmord  14175  faclbnd4lem4  14303  ccatval21sw  14593  lswccatn0lsw  14599  ccatpfx  14708  ccatopth  14723  cshweqdifid  14827  lenegsq  15339  moddvds  16288  dvdscmulr  16309  dvdsmulcr  16310  dvds2add  16315  dvds2sub  16316  dvdsleabs  16336  divalg  16428  divalgb  16429  ndvdsadd  16435  gcdcllem3  16526  dvdslegcd  16529  modgcd  16557  absmulgcd  16574  odzval  16818  pcmul  16878  ressid2  17261  ressval2  17262  catcisolem  18134  prf1st  18227  prf2nd  18228  1st2ndprf  18229  curfuncf  18261  curf2ndf  18270  pltval  18353  pospo  18366  lubel  18537  isdlat  18545  submgmcl  18732  prdssgrpd  18758  issubmnd  18786  prdsmndd  18795  submcl  18837  grpinvid1  19024  grpinvid2  19025  mulgp1  19140  ghmlin  19252  ghmsub  19255  odlem2  19570  gexlem2  19613  lsmvalx  19670  efgtval  19754  cmncom  19829  lssvnegcl  21011  islss3  21014  prdslmodd  21024  zntoslem  21596  evlslem2  22120  evlseu  22124  maducoeval2  22688  madutpos  22690  madugsum  22691  madurid  22692  m2cpminvid  22801  pm2mpghm  22864  unopn  22951  ntrss  23103  innei  23173  t1sep2  23417  metustsym  24603  cncfi  24944  rrxds  25443  quotval  26344  abelthlem2  26483  mudivsum  27582  padicabv  27682  nosupfv  27758  nosupres  27759  noinffv  27773  sltssepc  27852  divsval  28270  axsegconlem1  29075  nsnlplig  30641  nsnlpligALT  30642  grpoinvid1  30688  grpoinvid2  30689  grpodivval  30695  ablo4  30710  ablonncan  30716  nvnpcan  30816  nvmeq0  30818  nvabs  30832  imsdval  30846  ipval  30863  nmorepnf  30928  blo3i  30962  blometi  30963  ipasslem5  30995  hvmulcan  31232  his5  31246  his7  31250  his2sub2  31253  hhssabloilem  31421  hhssnv  31424  fh1  31778  fh2  31779  cm2j  31780  homcl  31906  homco1  31961  homulass  31962  hoadddi  31963  hosubsub2  31972  braadd  32105  bramul  32106  lnopmul  32127  lnopli  32128  lnopaddmuli  32133  lnopsubmuli  32135  lnfnli  32200  lnfnaddmuli  32205  kbass2  32277  mdexchi  32495  xdivval  33057  resvid2  33477  resvval2  33478  fedgmullem2  33888  unitdivcld  34159  bnj229  35140  bnj546  35152  bnj570  35161  rankfilimb  35359  cusgredgex2  35434  loop1cycl  35448  cvmlift2lem7  35620  finminlem  36639  ivthALT  36656  topdifinffinlem  37802  lindsadd  38073  exidcl  38336  grposnOLD  38342  rngoneglmul  38403  rngonegrmul  38404  divrngcl  38417  crngocom  38461  crngm4  38463  inidl  38490  xrninxpex  38877  oposlem  39767  hlsuprexch  39966  ldilcnv  40700  ltrnu  40706  tgrpgrplem  41334  tgrpabl  41336  erngdvlem3  41575  erngdvlem3-rN  41583  dvalveclem  41610  dvhfvadd  41676  dvhgrp  41692  dvhlveclem  41693  djhval2  41984  fmpocos  42813  resubadd  42949  diophren  43351  monotoddzzfi  43480  ltrmynn0  43486  ltrmxnn0  43487  lermxnn0  43488  rmyeq  43492  lermy  43493  jm2.21  43532  radcnvrat  44851  dvconstbi  44871  expgrowth  44872  bi3impb  45021  xlimmnfvlem2  46368  xlimpnfvlem2  46372  fnotaovb  47753  tposcurf1  49881  precofvalALT  49950  onetansqsecsq  50343