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  3517  vtocl3g  3519  rspc2ev  3578  reuss  4268  frc  5585  trssord  6332  funtp  6547  resdif  6793  f1cdmsn  7228  f1ofvswap  7252  fnotovb  7410  fovcdm  7528  fnovrn  7533  fmpoco  8036  smoord  8296  odi  8505  oeoa  8524  oeoe  8526  nndi  8550  ecopovtrn  8758  ecovass  8762  ecovdi  8763  unfi  9096  entrfil  9110  domtrfil  9117  f1imaenfi  9120  suppr  9376  infpr  9409  harval2  9910  fin23lem31  10254  tskuni  10695  addasspi  10807  mulasspi  10809  distrpi  10810  mulcanenq  10872  genpass  10921  distrlem1pr  10937  prlem934  10945  ltapr  10957  le2tri3i  11264  subadd  11384  addsub  11392  subdi  11571  submul2  11578  ltaddsub  11612  leaddsub  11614  divval  11799  diveq0  11807  div12  11819  diveq1  11827  divneg  11834  divdiv2  11854  ltmulgt11  12002  gt0div  12009  ge0div  12010  uzind3  12587  fnn0ind  12592  qdivcl  12884  irrmul  12888  xrlttr  13055  fzen  13458  modcyc  13827  modcyc2  13828  rpexpmord  14092  faclbnd4lem4  14220  ccatval21sw  14510  lswccatn0lsw  14516  ccatpfx  14625  ccatopth  14640  cshweqdifid  14744  lenegsq  15245  moddvds  16191  dvdscmulr  16212  dvdsmulcr  16213  dvds2add  16218  dvds2sub  16219  dvdsleabs  16239  divalg  16331  divalgb  16332  ndvdsadd  16338  gcdcllem3  16429  dvdslegcd  16432  modgcd  16460  absmulgcd  16477  odzval  16720  pcmul  16780  ressid2  17162  ressval2  17163  catcisolem  18035  prf1st  18128  prf2nd  18129  1st2ndprf  18130  curfuncf  18162  curf2ndf  18171  pltval  18254  pospo  18267  lubel  18438  isdlat  18446  submgmcl  18633  prdssgrpd  18659  issubmnd  18687  prdsmndd  18696  submcl  18738  grpinvid1  18925  grpinvid2  18926  mulgp1  19041  ghmlin  19154  ghmsub  19157  odlem2  19472  gexlem2  19515  lsmvalx  19572  efgtval  19656  cmncom  19731  lssvnegcl  20909  islss3  20912  prdslmodd  20922  zntoslem  21513  evlslem2  22035  evlseu  22039  maducoeval2  22583  madutpos  22585  madugsum  22586  madurid  22587  m2cpminvid  22696  pm2mpghm  22759  unopn  22846  ntrss  22998  innei  23068  t1sep2  23312  metustsym  24498  cncfi  24839  rrxds  25338  quotval  26240  abelthlem2  26382  mudivsum  27481  padicabv  27581  nosupfv  27658  nosupres  27659  noinffv  27673  sltssepc  27751  divsval  28169  axsegconlem1  28974  nsnlplig  30541  nsnlpligALT  30542  grpoinvid1  30588  grpoinvid2  30589  grpodivval  30595  ablo4  30610  ablonncan  30616  nvnpcan  30716  nvmeq0  30718  nvabs  30732  imsdval  30746  ipval  30763  nmorepnf  30828  blo3i  30862  blometi  30863  ipasslem5  30895  hvmulcan  31132  his5  31146  his7  31150  his2sub2  31153  hhssabloilem  31321  hhssnv  31324  fh1  31678  fh2  31679  cm2j  31680  homcl  31806  homco1  31861  homulass  31862  hoadddi  31863  hosubsub2  31872  braadd  32005  bramul  32006  lnopmul  32027  lnopli  32028  lnopaddmuli  32033  lnopsubmuli  32035  lnfnli  32100  lnfnaddmuli  32105  kbass2  32177  mdexchi  32395  xdivval  32983  resvid2  33395  resvval2  33396  fedgmullem2  33780  unitdivcld  34051  bnj229  35032  bnj546  35044  bnj570  35053  rankfilimb  35251  cusgredgex2  35311  loop1cycl  35325  cvmlift2lem7  35497  finminlem  36506  ivthALT  36523  topdifinffinlem  37659  lindsadd  37925  exidcl  38188  grposnOLD  38194  rngoneglmul  38255  rngonegrmul  38256  divrngcl  38269  crngocom  38313  crngm4  38315  inidl  38342  xrninxpex  38729  oposlem  39619  hlsuprexch  39818  ldilcnv  40552  ltrnu  40558  tgrpgrplem  41186  tgrpabl  41188  erngdvlem3  41427  erngdvlem3-rN  41435  dvalveclem  41462  dvhfvadd  41528  dvhgrp  41544  dvhlveclem  41545  djhval2  41836  f1o2d2  42666  fmpocos  42667  resubadd  42810  diophren  43244  monotoddzzfi  43373  ltrmynn0  43379  ltrmxnn0  43380  lermxnn0  43381  rmyeq  43385  lermy  43386  jm2.21  43425  radcnvrat  44744  dvconstbi  44764  expgrowth  44765  bi3impb  44914  xlimmnfvlem2  46265  xlimpnfvlem2  46269  fnotaovb  47632  tposcurf1  49732  precofvalALT  49801  onetansqsecsq  50194