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  3305  vtocl3gf  3571  rspc2ev  3635  reuss  4284  frc  5516  trssord  6203  funtp  6406  resdif  6630  fnotovb  7200  fovrn  7312  fnovrn  7317  fmpoco  7784  smoord  7996  odi  8199  oeoa  8217  oeoe  8219  nndi  8243  ecopovtrn  8394  ecovass  8398  ecovdi  8399  suppr  8929  infpr  8961  harval2  9420  fin23lem31  9759  tskuni  10199  addasspi  10311  mulasspi  10313  distrpi  10314  mulcanenq  10376  genpass  10425  distrlem1pr  10441  prlem934  10449  ltapr  10461  le2tri3i  10764  subadd  10883  addsub  10891  subdi  11067  submul2  11074  ltaddsub  11108  leaddsub  11110  divval  11294  div12  11314  diveq1  11325  divneg  11326  divdiv2  11346  ltmulgt11  11494  gt0div  11500  ge0div  11501  uzind3  12070  fnn0ind  12075  qdivcl  12363  irrmul  12367  xrlttr  12527  fzen  12918  modcyc  13268  modcyc2  13269  rpexpmord  13526  faclbnd4lem4  13650  ccatval21sw  13933  lswccatn0lsw  13939  ccatpfx  14057  ccatopth  14072  cshweqdifid  14176  lenegsq  14674  moddvds  15612  dvdscmulr  15632  dvdsmulcr  15633  dvds2add  15637  dvds2sub  15638  dvdsleabs  15655  divalg  15748  divalgb  15749  ndvdsadd  15755  gcdcllem3  15844  dvdslegcd  15847  modgcd  15874  absmulgcd  15891  odzval  16122  pcmul  16182  ressid2  16546  ressval2  16547  catcisolem  17360  prf1st  17448  prf2nd  17449  1st2ndprf  17450  curfuncf  17482  curf2ndf  17491  pltval  17564  pospo  17577  lubel  17726  isdlat  17797  issubmnd  17932  prdsmndd  17938  submcl  17971  grpinvid1  18148  grpinvid2  18149  mulgp1  18254  ghmlin  18357  ghmsub  18360  odlem2  18661  gexlem2  18701  lsmvalx  18758  efgtval  18843  cmncom  18917  lssvnegcl  19722  islss3  19725  prdslmodd  19735  evlslem2  20286  evlseu  20290  zntoslem  20697  maducoeval2  21243  madutpos  21245  madugsum  21246  madurid  21247  m2cpminvid  21355  pm2mpghm  21418  unopn  21505  ntrss  21657  innei  21727  t1sep2  21971  metustsym  23159  cncfi  23496  rrxds  23990  quotval  24875  abelthlem2  25014  mudivsum  26100  padicabv  26200  axsegconlem1  26697  nsnlplig  28252  nsnlpligALT  28253  grpoinvid1  28299  grpoinvid2  28300  grpodivval  28306  ablo4  28321  ablonncan  28327  nvnpcan  28427  nvmeq0  28429  nvabs  28443  imsdval  28457  ipval  28474  nmorepnf  28539  blo3i  28573  blometi  28574  ipasslem5  28606  hvmulcan  28843  his5  28857  his7  28861  his2sub2  28864  hhssabloilem  29032  hhssnv  29035  fh1  29389  fh2  29390  cm2j  29391  homcl  29517  homco1  29572  homulass  29573  hoadddi  29574  hosubsub2  29583  braadd  29716  bramul  29717  lnopmul  29738  lnopli  29739  lnopaddmuli  29744  lnopsubmuli  29746  lnfnli  29811  lnfnaddmuli  29816  kbass2  29888  mdexchi  30106  xdivval  30590  resvid2  30896  resvval2  30897  fedgmullem2  31021  unitdivcld  31139  bnj229  32151  bnj546  32163  bnj570  32172  cusgredgex2  32364  loop1cycl  32379  cvmlift2lem7  32551  nosupfv  33201  nosupres  33202  finminlem  33661  ivthALT  33678  topdifinffinlem  34622  lindsadd  34879  exidcl  35148  grposnOLD  35154  rngoneglmul  35215  rngonegrmul  35216  divrngcl  35229  crngocom  35273  crngm4  35275  inidl  35302  xrninxpex  35636  oposlem  36312  hlsuprexch  36511  ldilcnv  37245  ltrnu  37251  tgrpgrplem  37879  tgrpabl  37881  erngdvlem3  38120  erngdvlem3-rN  38128  dvalveclem  38155  dvhfvadd  38221  dvhgrp  38237  dvhlveclem  38238  djhval2  38529  resubadd  39202  diophren  39403  monotoddzzfi  39532  ltrmynn0  39538  ltrmxnn0  39539  lermxnn0  39540  rmyeq  39544  lermy  39545  jm2.21  39584  radcnvrat  40639  dvconstbi  40659  expgrowth  40660  bi3impb  40810  eel132  41029  xlimmnfvlem2  42106  xlimpnfvlem2  42110  fnotaovb  43390  submgmcl  44054  onetansqsecsq  44853