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  1131  3impdi  1349  rsp2e  3275  vtocl3gf  3572  vtocl3g  3574  rspc2ev  3634  reuss  4332  frc  5651  trssord  6402  funtp  6624  resdif  6869  f1cdmsn  7301  f1ofvswap  7325  fnotovb  7482  fovcdm  7602  fnovrn  7607  fmpoco  8118  smoord  8403  odi  8615  oeoa  8633  oeoe  8635  nndi  8659  ecopovtrn  8858  ecovass  8862  ecovdi  8863  unfi  9209  entrfil  9222  domtrfil  9229  f1imaenfi  9232  suppr  9508  infpr  9540  harval2  10034  fin23lem31  10380  tskuni  10820  addasspi  10932  mulasspi  10934  distrpi  10935  mulcanenq  10997  genpass  11046  distrlem1pr  11062  prlem934  11070  ltapr  11082  le2tri3i  11388  subadd  11508  addsub  11516  subdi  11693  submul2  11700  ltaddsub  11734  leaddsub  11736  divval  11921  diveq0  11929  div12  11941  diveq1  11949  divneg  11956  divdiv2  11976  ltmulgt11  12124  gt0div  12131  ge0div  12132  uzind3  12709  fnn0ind  12714  qdivcl  13009  irrmul  13013  xrlttr  13178  fzen  13577  modcyc  13942  modcyc2  13943  rpexpmord  14204  faclbnd4lem4  14331  ccatval21sw  14619  lswccatn0lsw  14625  ccatpfx  14735  ccatopth  14750  cshweqdifid  14854  lenegsq  15355  moddvds  16297  dvdscmulr  16318  dvdsmulcr  16319  dvds2add  16323  dvds2sub  16324  dvdsleabs  16344  divalg  16436  divalgb  16437  ndvdsadd  16443  gcdcllem3  16534  dvdslegcd  16537  modgcd  16565  absmulgcd  16582  odzval  16824  pcmul  16884  ressid2  17277  ressval2  17278  catcisolem  18163  prf1st  18259  prf2nd  18260  1st2ndprf  18261  curfuncf  18294  curf2ndf  18303  pltval  18389  pospo  18402  lubel  18571  isdlat  18579  submgmcl  18732  prdssgrpd  18758  issubmnd  18786  prdsmndd  18795  submcl  18837  grpinvid1  19021  grpinvid2  19022  mulgp1  19137  ghmlin  19251  ghmsub  19254  odlem2  19571  gexlem2  19614  lsmvalx  19671  efgtval  19755  cmncom  19830  lssvnegcl  20971  islss3  20974  prdslmodd  20984  zntoslem  21592  evlslem2  22120  evlseu  22124  maducoeval2  22661  madutpos  22663  madugsum  22664  madurid  22665  m2cpminvid  22774  pm2mpghm  22837  unopn  22924  ntrss  23078  innei  23148  t1sep2  23392  metustsym  24583  cncfi  24933  rrxds  25440  quotval  26348  abelthlem2  26490  mudivsum  27588  padicabv  27688  nosupfv  27765  nosupres  27766  noinffv  27780  ssltsepc  27852  divsval  28229  axsegconlem1  28946  nsnlplig  30509  nsnlpligALT  30510  grpoinvid1  30556  grpoinvid2  30557  grpodivval  30563  ablo4  30578  ablonncan  30584  nvnpcan  30684  nvmeq0  30686  nvabs  30700  imsdval  30714  ipval  30731  nmorepnf  30796  blo3i  30830  blometi  30831  ipasslem5  30863  hvmulcan  31100  his5  31114  his7  31118  his2sub2  31121  hhssabloilem  31289  hhssnv  31292  fh1  31646  fh2  31647  cm2j  31648  homcl  31774  homco1  31829  homulass  31830  hoadddi  31831  hosubsub2  31840  braadd  31973  bramul  31974  lnopmul  31995  lnopli  31996  lnopaddmuli  32001  lnopsubmuli  32003  lnfnli  32068  lnfnaddmuli  32073  kbass2  32145  mdexchi  32363  xdivval  32885  resvid2  33333  resvval2  33334  fedgmullem2  33657  unitdivcld  33861  bnj229  34876  bnj546  34888  bnj570  34897  cusgredgex2  35106  loop1cycl  35121  cvmlift2lem7  35293  finminlem  36300  ivthALT  36317  topdifinffinlem  37329  lindsadd  37599  exidcl  37862  grposnOLD  37868  rngoneglmul  37929  rngonegrmul  37930  divrngcl  37943  crngocom  37987  crngm4  37989  inidl  38016  xrninxpex  38375  oposlem  39163  hlsuprexch  39363  ldilcnv  40097  ltrnu  40103  tgrpgrplem  40731  tgrpabl  40733  erngdvlem3  40972  erngdvlem3-rN  40980  dvalveclem  41007  dvhfvadd  41073  dvhgrp  41089  dvhlveclem  41090  djhval2  41381  f1o2d2  42252  fmpocos  42253  resubadd  42385  diophren  42800  monotoddzzfi  42930  ltrmynn0  42936  ltrmxnn0  42937  lermxnn0  42938  rmyeq  42942  lermy  42943  jm2.21  42982  radcnvrat  44309  dvconstbi  44329  expgrowth  44330  bi3impb  44480  eel132  44699  xlimmnfvlem2  45788  xlimpnfvlem2  45792  fnotaovb  47147  onetansqsecsq  48991