Theorem 3impb 1114

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3adant3  1132  syl3an132  1166  3impdi  1351  rsp2e  3260  vtocl3gf  3552  vtocl3g  3554  rspc2ev  3614  reuss  4302  frc  5617  trssord  6369  funtp  6592  resdif  6838  f1cdmsn  7274  f1ofvswap  7298  fnotovb  7455  fovcdm  7575  fnovrn  7580  fmpoco  8092  smoord  8377  odi  8589  oeoa  8607  oeoe  8609  nndi  8633  ecopovtrn  8832  ecovass  8836  ecovdi  8837  unfi  9183  entrfil  9197  domtrfil  9204  f1imaenfi  9207  suppr  9482  infpr  9515  harval2  10009  fin23lem31  10355  tskuni  10795  addasspi  10907  mulasspi  10909  distrpi  10910  mulcanenq  10972  genpass  11021  distrlem1pr  11037  prlem934  11045  ltapr  11057  le2tri3i  11363  subadd  11483  addsub  11491  subdi  11668  submul2  11675  ltaddsub  11709  leaddsub  11711  divval  11896  diveq0  11904  div12  11916  diveq1  11924  divneg  11931  divdiv2  11951  ltmulgt11  12099  gt0div  12106  ge0div  12107  uzind3  12685  fnn0ind  12690  qdivcl  12984  irrmul  12988  xrlttr  13154  fzen  13556  modcyc  13921  modcyc2  13922  rpexpmord  14184  faclbnd4lem4  14312  ccatval21sw  14601  lswccatn0lsw  14607  ccatpfx  14717  ccatopth  14732  cshweqdifid  14836  lenegsq  15337  moddvds  16281  dvdscmulr  16302  dvdsmulcr  16303  dvds2add  16307  dvds2sub  16308  dvdsleabs  16328  divalg  16420  divalgb  16421  ndvdsadd  16427  gcdcllem3  16518  dvdslegcd  16521  modgcd  16549  absmulgcd  16566  odzval  16809  pcmul  16869  ressid2  17253  ressval2  17254  catcisolem  18121  prf1st  18214  prf2nd  18215  1st2ndprf  18216  curfuncf  18248  curf2ndf  18257  pltval  18340  pospo  18353  lubel  18522  isdlat  18530  submgmcl  18683  prdssgrpd  18709  issubmnd  18737  prdsmndd  18746  submcl  18788  grpinvid1  18972  grpinvid2  18973  mulgp1  19088  ghmlin  19202  ghmsub  19205  odlem2  19518  gexlem2  19561  lsmvalx  19618  efgtval  19702  cmncom  19777  lssvnegcl  20911  islss3  20914  prdslmodd  20924  zntoslem  21515  evlslem2  22035  evlseu  22039  maducoeval2  22576  madutpos  22578  madugsum  22579  madurid  22580  m2cpminvid  22689  pm2mpghm  22752  unopn  22839  ntrss  22991  innei  23061  t1sep2  23305  metustsym  24492  cncfi  24836  rrxds  25343  quotval  26250  abelthlem2  26392  mudivsum  27491  padicabv  27591  nosupfv  27668  nosupres  27669  noinffv  27683  ssltsepc  27755  divsval  28132  axsegconlem1  28842  nsnlplig  30408  nsnlpligALT  30409  grpoinvid1  30455  grpoinvid2  30456  grpodivval  30462  ablo4  30477  ablonncan  30483  nvnpcan  30583  nvmeq0  30585  nvabs  30599  imsdval  30613  ipval  30630  nmorepnf  30695  blo3i  30729  blometi  30730  ipasslem5  30762  hvmulcan  30999  his5  31013  his7  31017  his2sub2  31020  hhssabloilem  31188  hhssnv  31191  fh1  31545  fh2  31546  cm2j  31547  homcl  31673  homco1  31728  homulass  31729  hoadddi  31730  hosubsub2  31739  braadd  31872  bramul  31873  lnopmul  31894  lnopli  31895  lnopaddmuli  31900  lnopsubmuli  31902  lnfnli  31967  lnfnaddmuli  31972  kbass2  32044  mdexchi  32262  xdivval  32839  resvid2  33292  resvval2  33293  fedgmullem2  33616  unitdivcld  33878  bnj229  34861  bnj546  34873  bnj570  34882  cusgredgex2  35091  loop1cycl  35105  cvmlift2lem7  35277  finminlem  36282  ivthALT  36299  topdifinffinlem  37311  lindsadd  37583  exidcl  37846  grposnOLD  37852  rngoneglmul  37913  rngonegrmul  37914  divrngcl  37927  crngocom  37971  crngm4  37973  inidl  38000  xrninxpex  38358  oposlem  39146  hlsuprexch  39346  ldilcnv  40080  ltrnu  40086  tgrpgrplem  40714  tgrpabl  40716  erngdvlem3  40955  erngdvlem3-rN  40963  dvalveclem  40990  dvhfvadd  41056  dvhgrp  41072  dvhlveclem  41073  djhval2  41364  f1o2d2  42231  fmpocos  42232  resubadd  42369  diophren  42783  monotoddzzfi  42913  ltrmynn0  42919  ltrmxnn0  42920  lermxnn0  42921  rmyeq  42925  lermy  42926  jm2.21  42965  radcnvrat  44286  dvconstbi  44306  expgrowth  44307  bi3impb  44457  xlimmnfvlem2  45810  xlimpnfvlem2  45814  fnotaovb  47175  tposcurf1  49158  precofvalALT  49227  onetansqsecsq  49573