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 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1110	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3adant3  1131  3impdi  1349  rsp2e  3239  vtocl3gf  3510  vtocl3g  3512  rspc2ev  3573  reuss  4251  frc  5556  trssord  6287  funtp  6498  resdif  6746  f1cdmsn  7163  f1ofvswap  7187  fnotovb  7334  fovrn  7451  fnovrn  7456  fmpoco  7944  smoord  8205  odi  8419  oeoa  8437  oeoe  8439  nndi  8463  ecopovtrn  8618  ecovass  8622  ecovdi  8623  unfi  8964  entrfil  8980  domtrfil  8987  f1imaenfi  8990  suppr  9239  infpr  9271  harval2  9764  fin23lem31  10108  tskuni  10548  addasspi  10660  mulasspi  10662  distrpi  10663  mulcanenq  10725  genpass  10774  distrlem1pr  10790  prlem934  10798  ltapr  10810  le2tri3i  11114  subadd  11233  addsub  11241  subdi  11417  submul2  11424  ltaddsub  11458  leaddsub  11460  divval  11644  div12  11664  diveq1  11675  divneg  11676  divdiv2  11696  ltmulgt11  11844  gt0div  11850  ge0div  11851  uzind3  12423  fnn0ind  12428  qdivcl  12719  irrmul  12723  xrlttr  12883  fzen  13282  modcyc  13635  modcyc2  13636  rpexpmord  13895  faclbnd4lem4  14019  ccatval21sw  14299  lswccatn0lsw  14305  ccatpfx  14423  ccatopth  14438  cshweqdifid  14542  lenegsq  15041  moddvds  15983  dvdscmulr  16003  dvdsmulcr  16004  dvds2add  16008  dvds2sub  16009  dvdsleabs  16029  divalg  16121  divalgb  16122  ndvdsadd  16128  gcdcllem3  16217  dvdslegcd  16220  modgcd  16249  absmulgcd  16266  odzval  16501  pcmul  16561  ressid2  16954  ressval2  16955  catcisolem  17834  prf1st  17930  prf2nd  17931  1st2ndprf  17932  curfuncf  17965  curf2ndf  17974  pltval  18059  pospo  18072  lubel  18241  isdlat  18249  issubmnd  18421  prdsmndd  18427  submcl  18460  grpinvid1  18639  grpinvid2  18640  mulgp1  18745  ghmlin  18848  ghmsub  18851  odlem2  19156  gexlem2  19196  lsmvalx  19253  efgtval  19338  cmncom  19412  lssvnegcl  20227  islss3  20230  prdslmodd  20240  zntoslem  20773  evlslem2  21298  evlseu  21302  maducoeval2  21798  madutpos  21800  madugsum  21801  madurid  21802  m2cpminvid  21911  pm2mpghm  21974  unopn  22061  ntrss  22215  innei  22285  t1sep2  22529  metustsym  23720  cncfi  24066  rrxds  24566  quotval  25461  abelthlem2  25600  mudivsum  26687  padicabv  26787  axsegconlem1  27294  nsnlplig  28852  nsnlpligALT  28853  grpoinvid1  28899  grpoinvid2  28900  grpodivval  28906  ablo4  28921  ablonncan  28927  nvnpcan  29027  nvmeq0  29029  nvabs  29043  imsdval  29057  ipval  29074  nmorepnf  29139  blo3i  29173  blometi  29174  ipasslem5  29206  hvmulcan  29443  his5  29457  his7  29461  his2sub2  29464  hhssabloilem  29632  hhssnv  29635  fh1  29989  fh2  29990  cm2j  29991  homcl  30117  homco1  30172  homulass  30173  hoadddi  30174  hosubsub2  30183  braadd  30316  bramul  30317  lnopmul  30338  lnopli  30339  lnopaddmuli  30344  lnopsubmuli  30346  lnfnli  30411  lnfnaddmuli  30416  kbass2  30488  mdexchi  30706  xdivval  31202  resvid2  31536  resvval2  31537  fedgmullem2  31720  unitdivcld  31860  bnj229  32873  bnj546  32885  bnj570  32894  cusgredgex2  33093  loop1cycl  33108  cvmlift2lem7  33280  nosupfv  33918  nosupres  33919  noinffv  33933  ssltsepc  33996  finminlem  34516  ivthALT  34533  topdifinffinlem  35527  lindsadd  35779  exidcl  36043  grposnOLD  36049  rngoneglmul  36110  rngonegrmul  36111  divrngcl  36124  crngocom  36168  crngm4  36170  inidl  36197  xrninxpex  36527  oposlem  37203  hlsuprexch  37402  ldilcnv  38136  ltrnu  38142  tgrpgrplem  38770  tgrpabl  38772  erngdvlem3  39011  erngdvlem3-rN  39019  dvalveclem  39046  dvhfvadd  39112  dvhgrp  39128  dvhlveclem  39129  djhval2  39420  resubadd  40369  diophren  40642  monotoddzzfi  40771  ltrmynn0  40777  ltrmxnn0  40778  lermxnn0  40779  rmyeq  40783  lermy  40784  jm2.21  40823  radcnvrat  41939  dvconstbi  41959  expgrowth  41960  bi3impb  42110  eel132  42329  xlimmnfvlem2  43381  xlimpnfvlem2  43385  fnotaovb  44701  submgmcl  45359  onetansqsecsq  46474