Theorem 3impb 1120

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3adant3  1138  syl3an132  1172  3impdi  1357  rsp2e  3257  vtocl3gf  3516  vtocl3g  3518  rspc2ev  3573  reuss  4255  frc  5581  trssord  6327  funtp  6542  resdif  6788  f1cdmsn  7226  f1ofvswap  7250  fnotovb  7408  fovcdm  7526  fnovrn  7531  fmpoco  8034  mpof1o2d  8065  smoord  8295  odi  8504  oeoa  8523  oeoe  8525  nndi  8549  ecopovtrn  8757  ecovass  8761  ecovdi  8762  unfi  9095  entrfil  9109  domtrfil  9116  f1imaenfi  9119  suppr  9375  infpr  9408  harval2  9912  fin23lem31  10256  tskuni  10697  addasspi  10809  mulasspi  10811  distrpi  10812  mulcanenq  10874  genpass  10923  distrlem1pr  10939  prlem934  10947  ltapr  10959  le2tri3i  11267  subadd  11387  addsub  11395  subdi  11574  submul2  11581  ltaddsub  11615  leaddsub  11617  divval  11802  diveq0  11810  div12  11822  diveq1  11830  divneg  11837  divdiv2  11858  ltmulgt11  12006  gt0div  12013  ge0div  12014  uzind3  12614  fnn0ind  12619  qdivcl  12911  irrmul  12915  xrlttr  13082  fzen  13486  modcyc  13856  modcyc2  13857  rpexpmord  14121  faclbnd4lem4  14249  ccatval21sw  14539  lswccatn0lsw  14545  ccatpfx  14654  ccatopth  14669  cshweqdifid  14773  lenegsq  15274  moddvds  16223  dvdscmulr  16244  dvdsmulcr  16245  dvds2add  16250  dvds2sub  16251  dvdsleabs  16271  divalg  16363  divalgb  16364  ndvdsadd  16370  gcdcllem3  16461  dvdslegcd  16464  modgcd  16492  absmulgcd  16509  odzval  16753  pcmul  16813  ressid2  17195  ressval2  17196  catcisolem  18068  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  curf2ndf  18204  pltval  18287  pospo  18300  lubel  18471  isdlat  18479  submgmcl  18666  prdssgrpd  18692  issubmnd  18720  prdsmndd  18729  submcl  18771  grpinvid1  18958  grpinvid2  18959  mulgp1  19074  ghmlin  19187  ghmsub  19190  odlem2  19505  gexlem2  19548  lsmvalx  19605  efgtval  19689  cmncom  19764  lssvnegcl  20946  islss3  20949  prdslmodd  20959  zntoslem  21531  evlslem2  22055  evlseu  22059  maducoeval2  22623  madutpos  22625  madugsum  22626  madurid  22627  m2cpminvid  22736  pm2mpghm  22799  unopn  22886  ntrss  23038  innei  23108  t1sep2  23352  metustsym  24538  cncfi  24879  rrxds  25378  quotval  26276  abelthlem2  26415  mudivsum  27511  padicabv  27611  nosupfv  27688  nosupres  27689  noinffv  27703  sltssepc  27781  divsval  28199  axsegconlem1  29004  nsnlplig  30570  nsnlpligALT  30571  grpoinvid1  30617  grpoinvid2  30618  grpodivval  30624  ablo4  30639  ablonncan  30645  nvnpcan  30745  nvmeq0  30747  nvabs  30761  imsdval  30775  ipval  30792  nmorepnf  30857  blo3i  30891  blometi  30892  ipasslem5  30924  hvmulcan  31161  his5  31175  his7  31179  his2sub2  31182  hhssabloilem  31350  hhssnv  31353  fh1  31707  fh2  31708  cm2j  31709  homcl  31835  homco1  31890  homulass  31891  hoadddi  31892  hosubsub2  31901  braadd  32034  bramul  32035  lnopmul  32056  lnopli  32057  lnopaddmuli  32062  lnopsubmuli  32064  lnfnli  32129  lnfnaddmuli  32134  kbass2  32206  mdexchi  32424  xdivval  32997  resvid2  33413  resvval2  33414  fedgmullem2  33814  unitdivcld  34085  bnj229  35066  bnj546  35078  bnj570  35087  rankfilimb  35283  cusgredgex2  35351  loop1cycl  35365  cvmlift2lem7  35537  finminlem  36546  ivthALT  36563  topdifinffinlem  37709  lindsadd  37980  exidcl  38243  grposnOLD  38249  rngoneglmul  38310  rngonegrmul  38311  divrngcl  38324  crngocom  38368  crngm4  38370  inidl  38397  xrninxpex  38784  oposlem  39674  hlsuprexch  39873  ldilcnv  40607  ltrnu  40613  tgrpgrplem  41241  tgrpabl  41243  erngdvlem3  41482  erngdvlem3-rN  41490  dvalveclem  41517  dvhfvadd  41583  dvhgrp  41599  dvhlveclem  41600  djhval2  41891  fmpocos  42720  resubadd  42856  diophren  43258  monotoddzzfi  43387  ltrmynn0  43393  ltrmxnn0  43394  lermxnn0  43395  rmyeq  43399  lermy  43400  jm2.21  43439  radcnvrat  44758  dvconstbi  44778  expgrowth  44779  bi3impb  44928  xlimmnfvlem2  46276  xlimpnfvlem2  46280  fnotaovb  47661  tposcurf1  49789  precofvalALT  49858  onetansqsecsq  50251