Theorem 3impb 1113

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

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

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 396  df-3an 1087

This theorem is referenced by:  3adant3  1130  3impdi  1348  rsp2e  3233  vtocl3gf  3499  vtocl3g  3501  rspc2ev  3564  reuss  4247  frc  5546  trssord  6268  funtp  6475  resdif  6720  f1ofvswap  7158  fnotovb  7305  fovrn  7420  fnovrn  7425  fmpoco  7906  smoord  8167  odi  8372  oeoa  8390  oeoe  8392  nndi  8416  ecopovtrn  8567  ecovass  8571  ecovdi  8572  unfi  8917  entrfil  8931  domtrfi  8938  f1imaenfi  8939  suppr  9160  infpr  9192  harval2  9686  fin23lem31  10030  tskuni  10470  addasspi  10582  mulasspi  10584  distrpi  10585  mulcanenq  10647  genpass  10696  distrlem1pr  10712  prlem934  10720  ltapr  10732  le2tri3i  11035  subadd  11154  addsub  11162  subdi  11338  submul2  11345  ltaddsub  11379  leaddsub  11381  divval  11565  div12  11585  diveq1  11596  divneg  11597  divdiv2  11617  ltmulgt11  11765  gt0div  11771  ge0div  11772  uzind3  12344  fnn0ind  12349  qdivcl  12639  irrmul  12643  xrlttr  12803  fzen  13202  modcyc  13554  modcyc2  13555  rpexpmord  13814  faclbnd4lem4  13938  ccatval21sw  14218  lswccatn0lsw  14224  ccatpfx  14342  ccatopth  14357  cshweqdifid  14461  lenegsq  14960  moddvds  15902  dvdscmulr  15922  dvdsmulcr  15923  dvds2add  15927  dvds2sub  15928  dvdsleabs  15948  divalg  16040  divalgb  16041  ndvdsadd  16047  gcdcllem3  16136  dvdslegcd  16139  modgcd  16168  absmulgcd  16185  odzval  16420  pcmul  16480  ressid2  16871  ressval2  16872  catcisolem  17741  prf1st  17837  prf2nd  17838  1st2ndprf  17839  curfuncf  17872  curf2ndf  17881  pltval  17965  pospo  17978  lubel  18147  isdlat  18155  issubmnd  18327  prdsmndd  18333  submcl  18366  grpinvid1  18545  grpinvid2  18546  mulgp1  18651  ghmlin  18754  ghmsub  18757  odlem2  19062  gexlem2  19102  lsmvalx  19159  efgtval  19244  cmncom  19318  lssvnegcl  20133  islss3  20136  prdslmodd  20146  zntoslem  20676  evlslem2  21199  evlseu  21203  maducoeval2  21697  madutpos  21699  madugsum  21700  madurid  21701  m2cpminvid  21810  pm2mpghm  21873  unopn  21960  ntrss  22114  innei  22184  t1sep2  22428  metustsym  23617  cncfi  23963  rrxds  24462  quotval  25357  abelthlem2  25496  mudivsum  26583  padicabv  26683  axsegconlem1  27188  nsnlplig  28744  nsnlpligALT  28745  grpoinvid1  28791  grpoinvid2  28792  grpodivval  28798  ablo4  28813  ablonncan  28819  nvnpcan  28919  nvmeq0  28921  nvabs  28935  imsdval  28949  ipval  28966  nmorepnf  29031  blo3i  29065  blometi  29066  ipasslem5  29098  hvmulcan  29335  his5  29349  his7  29353  his2sub2  29356  hhssabloilem  29524  hhssnv  29527  fh1  29881  fh2  29882  cm2j  29883  homcl  30009  homco1  30064  homulass  30065  hoadddi  30066  hosubsub2  30075  braadd  30208  bramul  30209  lnopmul  30230  lnopli  30231  lnopaddmuli  30236  lnopsubmuli  30238  lnfnli  30303  lnfnaddmuli  30308  kbass2  30380  mdexchi  30598  xdivval  31095  resvid2  31429  resvval2  31430  fedgmullem2  31613  unitdivcld  31753  bnj229  32764  bnj546  32776  bnj570  32785  cusgredgex2  32984  loop1cycl  32999  cvmlift2lem7  33171  nosupfv  33836  nosupres  33837  noinffv  33851  ssltsepc  33914  finminlem  34434  ivthALT  34451  topdifinffinlem  35445  lindsadd  35697  exidcl  35961  grposnOLD  35967  rngoneglmul  36028  rngonegrmul  36029  divrngcl  36042  crngocom  36086  crngm4  36088  inidl  36115  xrninxpex  36447  oposlem  37123  hlsuprexch  37322  ldilcnv  38056  ltrnu  38062  tgrpgrplem  38690  tgrpabl  38692  erngdvlem3  38931  erngdvlem3-rN  38939  dvalveclem  38966  dvhfvadd  39032  dvhgrp  39048  dvhlveclem  39049  djhval2  39340  resubadd  40283  diophren  40551  monotoddzzfi  40680  ltrmynn0  40686  ltrmxnn0  40687  lermxnn0  40688  rmyeq  40692  lermy  40693  jm2.21  40732  radcnvrat  41821  dvconstbi  41841  expgrowth  41842  bi3impb  41992  eel132  42211  xlimmnfvlem2  43264  xlimpnfvlem2  43268  fnotaovb  44577  submgmcl  45236  onetansqsecsq  46349