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  3256  vtocl3gf  3530  vtocl3g  3532  rspc2ev  3591  reuss  4281  frc  5595  trssord  6342  funtp  6557  resdif  6803  f1cdmsn  7238  f1ofvswap  7262  fnotovb  7420  fovcdm  7538  fnovrn  7543  fmpoco  8047  smoord  8307  odi  8516  oeoa  8535  oeoe  8537  nndi  8561  ecopovtrn  8769  ecovass  8773  ecovdi  8774  unfi  9107  entrfil  9121  domtrfil  9128  f1imaenfi  9131  suppr  9387  infpr  9420  harval2  9921  fin23lem31  10265  tskuni  10706  addasspi  10818  mulasspi  10820  distrpi  10821  mulcanenq  10883  genpass  10932  distrlem1pr  10948  prlem934  10956  ltapr  10968  le2tri3i  11275  subadd  11395  addsub  11403  subdi  11582  submul2  11589  ltaddsub  11623  leaddsub  11625  divval  11810  diveq0  11818  div12  11830  diveq1  11838  divneg  11845  divdiv2  11865  ltmulgt11  12013  gt0div  12020  ge0div  12021  uzind3  12598  fnn0ind  12603  qdivcl  12895  irrmul  12899  xrlttr  13066  fzen  13469  modcyc  13838  modcyc2  13839  rpexpmord  14103  faclbnd4lem4  14231  ccatval21sw  14521  lswccatn0lsw  14527  ccatpfx  14636  ccatopth  14651  cshweqdifid  14755  lenegsq  15256  moddvds  16202  dvdscmulr  16223  dvdsmulcr  16224  dvds2add  16229  dvds2sub  16230  dvdsleabs  16250  divalg  16342  divalgb  16343  ndvdsadd  16349  gcdcllem3  16440  dvdslegcd  16443  modgcd  16471  absmulgcd  16488  odzval  16731  pcmul  16791  ressid2  17173  ressval2  17174  catcisolem  18046  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfuncf  18173  curf2ndf  18182  pltval  18265  pospo  18278  lubel  18449  isdlat  18457  submgmcl  18644  prdssgrpd  18670  issubmnd  18698  prdsmndd  18707  submcl  18749  grpinvid1  18933  grpinvid2  18934  mulgp1  19049  ghmlin  19162  ghmsub  19165  odlem2  19480  gexlem2  19523  lsmvalx  19580  efgtval  19664  cmncom  19739  lssvnegcl  20919  islss3  20922  prdslmodd  20932  zntoslem  21523  evlslem2  22046  evlseu  22050  maducoeval2  22596  madutpos  22598  madugsum  22599  madurid  22600  m2cpminvid  22709  pm2mpghm  22772  unopn  22859  ntrss  23011  innei  23081  t1sep2  23325  metustsym  24511  cncfi  24855  rrxds  25361  quotval  26268  abelthlem2  26410  mudivsum  27509  padicabv  27609  nosupfv  27686  nosupres  27687  noinffv  27701  sltssepc  27779  divsval  28197  axsegconlem1  29002  nsnlplig  30568  nsnlpligALT  30569  grpoinvid1  30615  grpoinvid2  30616  grpodivval  30622  ablo4  30637  ablonncan  30643  nvnpcan  30743  nvmeq0  30745  nvabs  30759  imsdval  30773  ipval  30790  nmorepnf  30855  blo3i  30889  blometi  30890  ipasslem5  30922  hvmulcan  31159  his5  31173  his7  31177  his2sub2  31180  hhssabloilem  31348  hhssnv  31351  fh1  31705  fh2  31706  cm2j  31707  homcl  31833  homco1  31888  homulass  31889  hoadddi  31890  hosubsub2  31899  braadd  32032  bramul  32033  lnopmul  32054  lnopli  32055  lnopaddmuli  32060  lnopsubmuli  32062  lnfnli  32127  lnfnaddmuli  32132  kbass2  32204  mdexchi  32422  xdivval  33010  resvid2  33422  resvval2  33423  fedgmullem2  33807  unitdivcld  34078  bnj229  35059  bnj546  35071  bnj570  35080  rankfilimb  35277  cusgredgex2  35336  loop1cycl  35350  cvmlift2lem7  35522  finminlem  36531  ivthALT  36548  topdifinffinlem  37599  lindsadd  37861  exidcl  38124  grposnOLD  38130  rngoneglmul  38191  rngonegrmul  38192  divrngcl  38205  crngocom  38249  crngm4  38251  inidl  38278  xrninxpex  38665  oposlem  39555  hlsuprexch  39754  ldilcnv  40488  ltrnu  40494  tgrpgrplem  41122  tgrpabl  41124  erngdvlem3  41363  erngdvlem3-rN  41371  dvalveclem  41398  dvhfvadd  41464  dvhgrp  41480  dvhlveclem  41481  djhval2  41772  f1o2d2  42602  fmpocos  42603  resubadd  42746  diophren  43167  monotoddzzfi  43296  ltrmynn0  43302  ltrmxnn0  43303  lermxnn0  43304  rmyeq  43308  lermy  43309  jm2.21  43348  radcnvrat  44667  dvconstbi  44687  expgrowth  44688  bi3impb  44837  xlimmnfvlem2  46188  xlimpnfvlem2  46192  fnotaovb  47555  tposcurf1  49655  precofvalALT  49724  onetansqsecsq  50117