Theorem 3expa 1181

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

Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  ad4ant123  1193  ad4ant124  1194  ad4ant134  1195  ad4ant234  1196  3anidm23  1275  mp3an2  1303  mpd3an3  1316  rgen3  2519  moi2  2865  sbc3ie  2982  preq12bg  3700  issod  4241  wepo  4281  reuhypd  4392  funimass4  5472  fvtp1g  5628  f1imass  5675  fcof1o  5690  f1ofveu  5762  f1ocnvfv3  5763  acexmid  5773  2ndrn  6081  frecrdg  6305  oawordriexmid  6366  mapxpen  6742  findcard  6782  findcard2  6783  findcard2s  6784  ltapig  7146  ltanqi  7210  ltmnqi  7211  lt2addnq  7212  lt2mulnq  7213  prarloclemcalc  7310  genpassl  7332  genpassu  7333  prmuloc  7374  ltexprlemm  7408  ltexprlemfl  7417  ltexprlemfu  7419  lteupri  7425  ltaprg  7427  mul4  7894  add4  7923  cnegexlem2  7938  cnegexlem3  7939  2addsub  7976  addsubeq4  7977  muladd  8146  ltleadd  8208  reapmul1  8357  apreim  8365  receuap  8430  p1le  8607  lemul12b  8619  lbinf  8706  zdiv  9139  fzind  9166  fnn0ind  9167  uzss  9346  qmulcl  9429  qreccl  9434  xrlttr  9581  xaddass  9652  icc0r  9709  iooshf  9735  elfz5  9798  elfz0fzfz0  9903  fzind2  10016  ioo0  10037  ico0  10039  ioc0  10040  expnegap0  10301  expineg2  10302  mulexpzap  10333  expsubap  10341  expnbnd  10415  facndiv  10485  bccmpl  10500  bcval5  10509  bcpasc  10512  crim  10630  climshftlemg  11071  2sumeq2dv  11140  hash2iun  11248  2cprodeq2dv  11337  dvdsval3  11497  dvdsnegb  11510  muldvds1  11518  muldvds2  11519  dvdscmul  11520  dvdsmulc  11521  dvds2ln  11526  divalgb  11622  ndvdssub  11627  gcddiv  11707  rpexp1i  11832  phiprmpw  11898  hashgcdeq  11904  innei  12332  iscnp4  12387  cnpnei  12388  cnnei  12401  cnconst  12403  ismeti  12515  isxmet2d  12517  elbl2ps  12561  elbl2  12562  xblpnfps  12567  xblpnf  12568  xblm  12586  blininf  12593  blssexps  12598  blssex  12599  blsscls2  12662  metss  12663  metrest  12675  metcn  12683  divcnap  12724  cdivcncfap  12756