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  2629  moi2  2997  sbc3ie  3115  2if2dc  3661  preq12bg  3876  issod  4439  wepo  4479  reuhypd  4591  funimass4  5726  fvtp1g  5891  f1imass  5946  fcof1o  5961  f1ofveu  6037  f1ocnvfv3  6038  acexmid  6048  2ndrn  6376  funsssuppss  6457  frecrdg  6638  oawordriexmid  6702  mapxpen  7100  findcard  7144  findcard2  7145  findcard2s  7146  ltapig  7652  ltanqi  7716  ltmnqi  7717  lt2addnq  7718  lt2mulnq  7719  prarloclemcalc  7816  genpassl  7838  genpassu  7839  prmuloc  7880  ltexprlemm  7914  ltexprlemfl  7923  ltexprlemfu  7925  lteupri  7931  ltaprg  7933  mul4  8404  add4  8433  cnegexlem2  8448  cnegexlem3  8449  2addsub  8486  addsubeq4  8487  muladd  8656  ltleadd  8719  reapmul1  8868  apreim  8876  receuap  8942  p1le  9122  lemul12b  9134  lbinf  9221  zdiv  9665  fzind  9692  fnn0ind  9693  uzss  9874  qmulcl  9968  qreccl  9973  xrlttr  10127  xaddass  10201  icc0r  10258  iooshf  10284  elfz5  10350  elfz0fzfz0  10459  fzind2  10584  ioo0  10618  ico0  10620  ioc0  10621  expnegap0  10908  expineg2  10909  mulexpzap  10940  expsubap  10948  expnbnd  11024  facndiv  11100  bccmpl  11115  bcval5  11124  bcpasc  11127  ccatrn  11293  swrdspsleq  11355  swrdccat2  11359  ccatpfx  11389  pfxccat1  11390  swrdswrd  11393  cats1un  11409  crim  11539  climshftlemg  11983  2sumeq2dv  12052  hash2iun  12161  2cprodeq2dv  12250  dvdsval3  12473  dvdsnegb  12490  muldvds1  12498  muldvds2  12499  dvdscmul  12500  dvdsmulc  12501  dvds2ln  12506  divalgb  12607  ndvdssub  12612  gcddiv  12711  rpexp1i  12847  phiprmpw  12915  hashgcdeq  12933  pythagtriplem1  12959  pockthg  13051  infpnlem1  13053  4sqlem3  13084  imasaddfnlemg  13519  mndpfo  13643  grplmulf1o  13779  grplactcnv  13807  mulgnn0subcl  13844  mulgsubcl  13845  mulgdir  13863  issubg2m  13898  issubgrpd2  13899  nmzsubg  13919  eqgen  13936  ghmmulg  13965  ghmf1  13982  kerf1ghm  13983  conjghm  13985  srglmhm  14129  srgrmhm  14130  ringlghm  14197  ringrghm  14198  oppr1g  14218  dvdsrcl2  14236  crngunit  14248  subsubrng  14351  subrgugrp  14377  subsubrg  14382  islmod  14431  lmodvsdir  14452  lmodvsass  14453  lsssubg  14517  lss1d  14523  lidlsubg  14626  lidlsubcl  14627  expghmap  14747  mulgghm2  14748  innei  15020  iscnp4  15075  cnpnei  15076  cnnei  15089  cnconst  15091  ismeti  15203  isxmet2d  15205  elbl2ps  15249  elbl2  15250  xblpnfps  15255  xblpnf  15256  xblm  15274  blininf  15281  blssexps  15286  blssex  15287  blsscls2  15350  metss  15351  metrest  15363  metcn  15371  divcnap  15422  cdivcncfap  15461  dvply1  15622  lgslem4  15868  lgscllem  15872  lgsneg1  15890  lgsne0  15903  uspgr2wlkeq  16352  eupth2lem3lem7fi  16461