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  3250  vtocl3gf  3524  vtocl3g  3526  rspc2ev  3585  reuss  4272  frc  5574  trssord  6318  funtp  6533  resdif  6779  f1cdmsn  7211  f1ofvswap  7235  fnotovb  7393  fovcdm  7511  fnovrn  7516  fmpoco  8020  smoord  8280  odi  8489  oeoa  8507  oeoe  8509  nndi  8533  ecopovtrn  8739  ecovass  8743  ecovdi  8744  unfi  9075  entrfil  9089  domtrfil  9096  f1imaenfi  9099  suppr  9351  infpr  9384  harval2  9885  fin23lem31  10229  tskuni  10669  addasspi  10781  mulasspi  10783  distrpi  10784  mulcanenq  10846  genpass  10895  distrlem1pr  10911  prlem934  10919  ltapr  10931  le2tri3i  11238  subadd  11358  addsub  11366  subdi  11545  submul2  11552  ltaddsub  11586  leaddsub  11588  divval  11773  diveq0  11781  div12  11793  diveq1  11801  divneg  11808  divdiv2  11828  ltmulgt11  11976  gt0div  11983  ge0div  11984  uzind3  12562  fnn0ind  12567  qdivcl  12863  irrmul  12867  xrlttr  13034  fzen  13436  modcyc  13805  modcyc2  13806  rpexpmord  14070  faclbnd4lem4  14198  ccatval21sw  14488  lswccatn0lsw  14494  ccatpfx  14603  ccatopth  14618  cshweqdifid  14722  lenegsq  15223  moddvds  16169  dvdscmulr  16190  dvdsmulcr  16191  dvds2add  16196  dvds2sub  16197  dvdsleabs  16217  divalg  16309  divalgb  16310  ndvdsadd  16316  gcdcllem3  16407  dvdslegcd  16410  modgcd  16438  absmulgcd  16455  odzval  16698  pcmul  16758  ressid2  17140  ressval2  17141  catcisolem  18012  prf1st  18105  prf2nd  18106  1st2ndprf  18107  curfuncf  18139  curf2ndf  18148  pltval  18231  pospo  18244  lubel  18415  isdlat  18423  submgmcl  18610  prdssgrpd  18636  issubmnd  18664  prdsmndd  18673  submcl  18715  grpinvid1  18899  grpinvid2  18900  mulgp1  19015  ghmlin  19128  ghmsub  19131  odlem2  19446  gexlem2  19489  lsmvalx  19546  efgtval  19630  cmncom  19705  lssvnegcl  20884  islss3  20887  prdslmodd  20897  zntoslem  21488  evlslem2  22009  evlseu  22013  maducoeval2  22550  madutpos  22552  madugsum  22553  madurid  22554  m2cpminvid  22663  pm2mpghm  22726  unopn  22813  ntrss  22965  innei  23035  t1sep2  23279  metustsym  24465  cncfi  24809  rrxds  25315  quotval  26222  abelthlem2  26364  mudivsum  27463  padicabv  27563  nosupfv  27640  nosupres  27641  noinffv  27655  ssltsepc  27729  divsval  28123  axsegconlem1  28890  nsnlplig  30453  nsnlpligALT  30454  grpoinvid1  30500  grpoinvid2  30501  grpodivval  30507  ablo4  30522  ablonncan  30528  nvnpcan  30628  nvmeq0  30630  nvabs  30644  imsdval  30658  ipval  30675  nmorepnf  30740  blo3i  30774  blometi  30775  ipasslem5  30807  hvmulcan  31044  his5  31058  his7  31062  his2sub2  31065  hhssabloilem  31233  hhssnv  31236  fh1  31590  fh2  31591  cm2j  31592  homcl  31718  homco1  31773  homulass  31774  hoadddi  31775  hosubsub2  31784  braadd  31917  bramul  31918  lnopmul  31939  lnopli  31940  lnopaddmuli  31945  lnopsubmuli  31947  lnfnli  32012  lnfnaddmuli  32017  kbass2  32089  mdexchi  32307  xdivval  32891  resvid2  33287  resvval2  33288  fedgmullem2  33635  unitdivcld  33906  bnj229  34888  bnj546  34900  bnj570  34909  rankfilimb  35105  cusgredgex2  35159  loop1cycl  35173  cvmlift2lem7  35345  finminlem  36352  ivthALT  36369  topdifinffinlem  37381  lindsadd  37653  exidcl  37916  grposnOLD  37922  rngoneglmul  37983  rngonegrmul  37984  divrngcl  37997  crngocom  38041  crngm4  38043  inidl  38070  xrninxpex  38426  oposlem  39221  hlsuprexch  39420  ldilcnv  40154  ltrnu  40160  tgrpgrplem  40788  tgrpabl  40790  erngdvlem3  41029  erngdvlem3-rN  41037  dvalveclem  41064  dvhfvadd  41130  dvhgrp  41146  dvhlveclem  41147  djhval2  41438  f1o2d2  42266  fmpocos  42267  resubadd  42412  diophren  42846  monotoddzzfi  42975  ltrmynn0  42981  ltrmxnn0  42982  lermxnn0  42983  rmyeq  42987  lermy  42988  jm2.21  43027  radcnvrat  44347  dvconstbi  44367  expgrowth  44368  bi3impb  44517  xlimmnfvlem2  45871  xlimpnfvlem2  45875  fnotaovb  47229  tposcurf1  49331  precofvalALT  49400  onetansqsecsq  49793