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  3247  vtocl3gf  3530  vtocl3g  3532  rspc2ev  3592  reuss  4280  frc  5586  trssord  6328  funtp  6543  resdif  6789  f1cdmsn  7223  f1ofvswap  7247  fnotovb  7405  fovcdm  7523  fnovrn  7528  fmpoco  8035  smoord  8295  odi  8504  oeoa  8522  oeoe  8524  nndi  8548  ecopovtrn  8754  ecovass  8758  ecovdi  8759  unfi  9095  entrfil  9109  domtrfil  9116  f1imaenfi  9119  suppr  9381  infpr  9414  harval2  9912  fin23lem31  10256  tskuni  10696  addasspi  10808  mulasspi  10810  distrpi  10811  mulcanenq  10873  genpass  10922  distrlem1pr  10938  prlem934  10946  ltapr  10958  le2tri3i  11265  subadd  11385  addsub  11393  subdi  11572  submul2  11579  ltaddsub  11613  leaddsub  11615  divval  11800  diveq0  11808  div12  11820  diveq1  11828  divneg  11835  divdiv2  11855  ltmulgt11  12003  gt0div  12010  ge0div  12011  uzind3  12589  fnn0ind  12594  qdivcl  12890  irrmul  12894  xrlttr  13061  fzen  13463  modcyc  13829  modcyc2  13830  rpexpmord  14094  faclbnd4lem4  14222  ccatval21sw  14511  lswccatn0lsw  14517  ccatpfx  14626  ccatopth  14641  cshweqdifid  14745  lenegsq  15247  moddvds  16193  dvdscmulr  16214  dvdsmulcr  16215  dvds2add  16220  dvds2sub  16221  dvdsleabs  16241  divalg  16333  divalgb  16334  ndvdsadd  16340  gcdcllem3  16431  dvdslegcd  16434  modgcd  16462  absmulgcd  16479  odzval  16722  pcmul  16782  ressid2  17164  ressval2  17165  catcisolem  18036  prf1st  18129  prf2nd  18130  1st2ndprf  18131  curfuncf  18163  curf2ndf  18172  pltval  18255  pospo  18268  lubel  18439  isdlat  18447  submgmcl  18600  prdssgrpd  18626  issubmnd  18654  prdsmndd  18663  submcl  18705  grpinvid1  18889  grpinvid2  18890  mulgp1  19005  ghmlin  19119  ghmsub  19122  odlem2  19437  gexlem2  19480  lsmvalx  19537  efgtval  19621  cmncom  19696  lssvnegcl  20878  islss3  20881  prdslmodd  20891  zntoslem  21482  evlslem2  22003  evlseu  22007  maducoeval2  22544  madutpos  22546  madugsum  22547  madurid  22548  m2cpminvid  22657  pm2mpghm  22720  unopn  22807  ntrss  22959  innei  23029  t1sep2  23273  metustsym  24460  cncfi  24804  rrxds  25310  quotval  26217  abelthlem2  26359  mudivsum  27458  padicabv  27558  nosupfv  27635  nosupres  27636  noinffv  27650  ssltsepc  27723  divsval  28116  axsegconlem1  28881  nsnlplig  30444  nsnlpligALT  30445  grpoinvid1  30491  grpoinvid2  30492  grpodivval  30498  ablo4  30513  ablonncan  30519  nvnpcan  30619  nvmeq0  30621  nvabs  30635  imsdval  30649  ipval  30666  nmorepnf  30731  blo3i  30765  blometi  30766  ipasslem5  30798  hvmulcan  31035  his5  31049  his7  31053  his2sub2  31056  hhssabloilem  31224  hhssnv  31227  fh1  31581  fh2  31582  cm2j  31583  homcl  31709  homco1  31764  homulass  31765  hoadddi  31766  hosubsub2  31775  braadd  31908  bramul  31909  lnopmul  31930  lnopli  31931  lnopaddmuli  31936  lnopsubmuli  31938  lnfnli  32003  lnfnaddmuli  32008  kbass2  32080  mdexchi  32298  xdivval  32878  resvid2  33287  resvval2  33288  fedgmullem2  33616  unitdivcld  33887  bnj229  34870  bnj546  34882  bnj570  34891  cusgredgex2  35115  loop1cycl  35129  cvmlift2lem7  35301  finminlem  36311  ivthALT  36328  topdifinffinlem  37340  lindsadd  37612  exidcl  37875  grposnOLD  37881  rngoneglmul  37942  rngonegrmul  37943  divrngcl  37956  crngocom  38000  crngm4  38002  inidl  38029  xrninxpex  38385  oposlem  39180  hlsuprexch  39380  ldilcnv  40114  ltrnu  40120  tgrpgrplem  40748  tgrpabl  40750  erngdvlem3  40989  erngdvlem3-rN  40997  dvalveclem  41024  dvhfvadd  41090  dvhgrp  41106  dvhlveclem  41107  djhval2  41398  f1o2d2  42226  fmpocos  42227  resubadd  42372  diophren  42806  monotoddzzfi  42935  ltrmynn0  42941  ltrmxnn0  42942  lermxnn0  42943  rmyeq  42947  lermy  42948  jm2.21  42987  radcnvrat  44307  dvconstbi  44327  expgrowth  44328  bi3impb  44478  xlimmnfvlem2  45834  xlimpnfvlem2  45838  fnotaovb  47202  tposcurf1  49304  precofvalALT  49373  onetansqsecsq  49766