Theorem 3expa 1203

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

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

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 980

This theorem is referenced by:  ad4ant123  1215  ad4ant124  1216  ad4ant134  1217  ad4ant234  1218  3anidm23  1297  mp3an2  1325  mpd3an3  1338  rgen3  2562  moi2  2916  sbc3ie  3034  preq12bg  3769  issod  4313  wepo  4353  reuhypd  4465  funimass4  5558  fvtp1g  5716  f1imass  5765  fcof1o  5780  f1ofveu  5853  f1ocnvfv3  5854  acexmid  5864  2ndrn  6174  frecrdg  6399  oawordriexmid  6461  mapxpen  6838  findcard  6878  findcard2  6879  findcard2s  6880  ltapig  7312  ltanqi  7376  ltmnqi  7377  lt2addnq  7378  lt2mulnq  7379  prarloclemcalc  7476  genpassl  7498  genpassu  7499  prmuloc  7540  ltexprlemm  7574  ltexprlemfl  7583  ltexprlemfu  7585  lteupri  7591  ltaprg  7593  mul4  8063  add4  8092  cnegexlem2  8107  cnegexlem3  8108  2addsub  8145  addsubeq4  8146  muladd  8315  ltleadd  8377  reapmul1  8526  apreim  8534  receuap  8599  p1le  8777  lemul12b  8789  lbinf  8876  zdiv  9312  fzind  9339  fnn0ind  9340  uzss  9519  qmulcl  9608  qreccl  9613  xrlttr  9764  xaddass  9838  icc0r  9895  iooshf  9921  elfz5  9985  elfz0fzfz0  10094  fzind2  10207  ioo0  10228  ico0  10230  ioc0  10231  expnegap0  10496  expineg2  10497  mulexpzap  10528  expsubap  10536  expnbnd  10611  facndiv  10685  bccmpl  10700  bcval5  10709  bcpasc  10712  crim  10833  climshftlemg  11276  2sumeq2dv  11345  hash2iun  11453  2cprodeq2dv  11542  dvdsval3  11764  dvdsnegb  11781  muldvds1  11789  muldvds2  11790  dvdscmul  11791  dvdsmulc  11792  dvds2ln  11797  divalgb  11895  ndvdssub  11900  gcddiv  11985  rpexp1i  12119  phiprmpw  12187  hashgcdeq  12204  pythagtriplem1  12230  pockthg  12320  infpnlem1  12322  4sqlem3  12353  mndpfo  12703  grplmulf1o  12803  grplactcnv  12831  mulgnn0subcl  12855  mulgsubcl  12856  mulgdir  12873  srglmhm  12969  srgrmhm  12970  innei  13214  iscnp4  13269  cnpnei  13270  cnnei  13283  cnconst  13285  ismeti  13397  isxmet2d  13399  elbl2ps  13443  elbl2  13444  xblpnfps  13449  xblpnf  13450  xblm  13468  blininf  13475  blssexps  13480  blssex  13481  blsscls2  13544  metss  13545  metrest  13557  metcn  13565  divcnap  13606  cdivcncfap  13638  lgslem4  13955  lgscllem  13959  lgsneg1  13977  lgsne0  13990