Theorem 3expa 1230

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expa	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem 3expa

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1229	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  ad4ant123  1242  ad4ant124  1243  ad4ant134  1244  ad4ant234  1245  ad5ant123  1266  3anidm23  1334  mp3an2  1362  mpd3an3  1375  rgen3  2620  moi2  2988  sbc3ie  3106  2if2dc  3649  preq12bg  3861  issod  4422  wepo  4462  reuhypd  4574  funimass4  5705  fvtp1g  5870  f1imass  5925  fcof1o  5940  f1ofveu  6016  f1ocnvfv3  6017  acexmid  6027  2ndrn  6355  funsssuppss  6436  frecrdg  6617  oawordriexmid  6681  mapxpen  7077  findcard  7120  findcard2  7121  findcard2s  7122  ltapig  7618  ltanqi  7682  ltmnqi  7683  lt2addnq  7684  lt2mulnq  7685  prarloclemcalc  7782  genpassl  7804  genpassu  7805  prmuloc  7846  ltexprlemm  7880  ltexprlemfl  7889  ltexprlemfu  7891  lteupri  7897  ltaprg  7899  mul4  8370  add4  8399  cnegexlem2  8414  cnegexlem3  8415  2addsub  8452  addsubeq4  8453  muladd  8622  ltleadd  8685  reapmul1  8834  apreim  8842  receuap  8908  p1le  9088  lemul12b  9100  lbinf  9187  zdiv  9629  fzind  9656  fnn0ind  9657  uzss  9838  qmulcl  9932  qreccl  9937  xrlttr  10091  xaddass  10165  icc0r  10222  iooshf  10248  elfz5  10314  elfz0fzfz0  10423  fzind2  10548  ioo0  10582  ico0  10584  ioc0  10585  expnegap0  10872  expineg2  10873  mulexpzap  10904  expsubap  10912  expnbnd  10988  facndiv  11064  bccmpl  11079  bcval5  11088  bcpasc  11091  ccatrn  11252  swrdspsleq  11314  swrdccat2  11318  ccatpfx  11348  pfxccat1  11349  swrdswrd  11352  cats1un  11368  crim  11498  climshftlemg  11942  2sumeq2dv  12011  hash2iun  12120  2cprodeq2dv  12209  dvdsval3  12432  dvdsnegb  12449  muldvds1  12457  muldvds2  12458  dvdscmul  12459  dvdsmulc  12460  dvds2ln  12465  divalgb  12566  ndvdssub  12571  gcddiv  12670  rpexp1i  12806  phiprmpw  12874  hashgcdeq  12892  pythagtriplem1  12918  pockthg  13010  infpnlem1  13012  4sqlem3  13043  imasaddfnlemg  13477  mndpfo  13601  grplmulf1o  13737  grplactcnv  13765  mulgnn0subcl  13802  mulgsubcl  13803  mulgdir  13821  issubg2m  13856  issubgrpd2  13857  nmzsubg  13877  eqgen  13894  ghmmulg  13923  ghmf1  13940  kerf1ghm  13941  conjghm  13943  srglmhm  14087  srgrmhm  14088  ringlghm  14155  ringrghm  14156  oppr1g  14176  dvdsrcl2  14194  crngunit  14206  subsubrng  14309  subrgugrp  14335  subsubrg  14340  islmod  14387  lmodvsdir  14408  lmodvsass  14409  lsssubg  14473  lss1d  14479  lidlsubg  14582  lidlsubcl  14583  expghmap  14703  mulgghm2  14704  innei  14974  iscnp4  15029  cnpnei  15030  cnnei  15043  cnconst  15045  ismeti  15157  isxmet2d  15159  elbl2ps  15203  elbl2  15204  xblpnfps  15209  xblpnf  15210  xblm  15228  blininf  15235  blssexps  15240  blssex  15241  blsscls2  15304  metss  15305  metrest  15317  metcn  15325  divcnap  15376  cdivcncfap  15415  dvply1  15576  lgslem4  15822  lgscllem  15826  lgsneg1  15844  lgsne0  15857  uspgr2wlkeq  16306  eupth2lem3lem7fi  16415