Theorem 3expa 1192

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

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

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 969

This theorem is referenced by:  ad4ant123  1204  ad4ant124  1205  ad4ant134  1206  ad4ant234  1207  3anidm23  1286  mp3an2  1314  mpd3an3  1327  rgen3  2551  moi2  2902  sbc3ie  3019  preq12bg  3747  issod  4291  wepo  4331  reuhypd  4443  funimass4  5531  fvtp1g  5687  f1imass  5736  fcof1o  5751  f1ofveu  5824  f1ocnvfv3  5825  acexmid  5835  2ndrn  6143  frecrdg  6367  oawordriexmid  6429  mapxpen  6805  findcard  6845  findcard2  6846  findcard2s  6847  ltapig  7270  ltanqi  7334  ltmnqi  7335  lt2addnq  7336  lt2mulnq  7337  prarloclemcalc  7434  genpassl  7456  genpassu  7457  prmuloc  7498  ltexprlemm  7532  ltexprlemfl  7541  ltexprlemfu  7543  lteupri  7549  ltaprg  7551  mul4  8021  add4  8050  cnegexlem2  8065  cnegexlem3  8066  2addsub  8103  addsubeq4  8104  muladd  8273  ltleadd  8335  reapmul1  8484  apreim  8492  receuap  8557  p1le  8735  lemul12b  8747  lbinf  8834  zdiv  9270  fzind  9297  fnn0ind  9298  uzss  9477  qmulcl  9566  qreccl  9571  xrlttr  9722  xaddass  9796  icc0r  9853  iooshf  9879  elfz5  9943  elfz0fzfz0  10051  fzind2  10164  ioo0  10185  ico0  10187  ioc0  10188  expnegap0  10453  expineg2  10454  mulexpzap  10485  expsubap  10493  expnbnd  10567  facndiv  10641  bccmpl  10656  bcval5  10665  bcpasc  10668  crim  10786  climshftlemg  11229  2sumeq2dv  11298  hash2iun  11406  2cprodeq2dv  11495  dvdsval3  11717  dvdsnegb  11734  muldvds1  11742  muldvds2  11743  dvdscmul  11744  dvdsmulc  11745  dvds2ln  11750  divalgb  11847  ndvdssub  11852  gcddiv  11937  rpexp1i  12063  phiprmpw  12131  hashgcdeq  12148  pythagtriplem1  12174  innei  12704  iscnp4  12759  cnpnei  12760  cnnei  12773  cnconst  12775  ismeti  12887  isxmet2d  12889  elbl2ps  12933  elbl2  12934  xblpnfps  12939  xblpnf  12940  xblm  12958  blininf  12965  blssexps  12970  blssex  12971  blsscls2  13034  metss  13035  metrest  13047  metcn  13055  divcnap  13096  cdivcncfap  13128