Theorem 3expa 1206

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 1205	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 256	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

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

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 983

This theorem is referenced by:  ad4ant123  1218  ad4ant124  1219  ad4ant134  1220  ad4ant234  1221  ad5ant123  1242  3anidm23  1310  mp3an2  1338  mpd3an3  1351  rgen3  2593  moi2  2954  sbc3ie  3072  preq12bg  3814  issod  4366  wepo  4406  reuhypd  4518  funimass4  5629  fvtp1g  5792  f1imass  5843  fcof1o  5858  f1ofveu  5932  f1ocnvfv3  5933  acexmid  5943  2ndrn  6269  frecrdg  6494  oawordriexmid  6556  mapxpen  6945  findcard  6985  findcard2  6986  findcard2s  6987  ltapig  7451  ltanqi  7515  ltmnqi  7516  lt2addnq  7517  lt2mulnq  7518  prarloclemcalc  7615  genpassl  7637  genpassu  7638  prmuloc  7679  ltexprlemm  7713  ltexprlemfl  7722  ltexprlemfu  7724  lteupri  7730  ltaprg  7732  mul4  8204  add4  8233  cnegexlem2  8248  cnegexlem3  8249  2addsub  8286  addsubeq4  8287  muladd  8456  ltleadd  8519  reapmul1  8668  apreim  8676  receuap  8742  p1le  8922  lemul12b  8934  lbinf  9021  zdiv  9461  fzind  9488  fnn0ind  9489  uzss  9669  qmulcl  9758  qreccl  9763  xrlttr  9917  xaddass  9991  icc0r  10048  iooshf  10074  elfz5  10139  elfz0fzfz0  10248  fzind2  10368  ioo0  10402  ico0  10404  ioc0  10405  expnegap0  10692  expineg2  10693  mulexpzap  10724  expsubap  10732  expnbnd  10808  facndiv  10884  bccmpl  10899  bcval5  10908  bcpasc  10911  ccatrn  11065  swrdspsleq  11120  swrdccat2  11124  crim  11169  climshftlemg  11613  2sumeq2dv  11682  hash2iun  11790  2cprodeq2dv  11879  dvdsval3  12102  dvdsnegb  12119  muldvds1  12127  muldvds2  12128  dvdscmul  12129  dvdsmulc  12130  dvds2ln  12135  divalgb  12236  ndvdssub  12241  gcddiv  12340  rpexp1i  12476  phiprmpw  12544  hashgcdeq  12562  pythagtriplem1  12588  pockthg  12680  infpnlem1  12682  4sqlem3  12713  imasaddfnlemg  13146  mndpfo  13270  grplmulf1o  13406  grplactcnv  13434  mulgnn0subcl  13471  mulgsubcl  13472  mulgdir  13490  issubg2m  13525  issubgrpd2  13526  nmzsubg  13546  eqgen  13563  ghmmulg  13592  ghmf1  13609  kerf1ghm  13610  conjghm  13612  srglmhm  13755  srgrmhm  13756  ringlghm  13823  ringrghm  13824  oppr1g  13844  dvdsrcl2  13861  crngunit  13873  subsubrng  13976  subrgugrp  14002  subsubrg  14007  islmod  14053  lmodvsdir  14074  lmodvsass  14075  lsssubg  14139  lss1d  14145  lidlsubg  14248  lidlsubcl  14249  expghmap  14369  mulgghm2  14370  innei  14635  iscnp4  14690  cnpnei  14691  cnnei  14704  cnconst  14706  ismeti  14818  isxmet2d  14820  elbl2ps  14864  elbl2  14865  xblpnfps  14870  xblpnf  14871  xblm  14889  blininf  14896  blssexps  14901  blssex  14902  blsscls2  14965  metss  14966  metrest  14978  metcn  14986  divcnap  15037  cdivcncfap  15076  dvply1  15237  lgslem4  15480  lgscllem  15484  lgsneg1  15502  lgsne0  15515