Theorem 3expa 1149

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

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

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

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

This theorem is referenced by:  ad4ant123  1161  ad4ant124  1162  ad4ant134  1163  ad4ant234  1164  3anidm23  1243  mp3an2  1271  mpd3an3  1284  rgen3  2478  moi2  2818  sbc3ie  2934  preq12bg  3647  issod  4179  wepo  4219  reuhypd  4330  funimass4  5404  fvtp1g  5560  f1imass  5607  fcof1o  5622  f1ofveu  5694  f1ocnvfv3  5695  acexmid  5705  2ndrn  6011  frecrdg  6235  oawordriexmid  6296  mapxpen  6671  findcard  6711  findcard2  6712  findcard2s  6713  ltapig  7047  ltanqi  7111  ltmnqi  7112  lt2addnq  7113  lt2mulnq  7114  prarloclemcalc  7211  genpassl  7233  genpassu  7234  prmuloc  7275  ltexprlemm  7309  ltexprlemfl  7318  ltexprlemfu  7320  lteupri  7326  ltaprg  7328  mul4  7765  add4  7794  cnegexlem2  7809  cnegexlem3  7810  2addsub  7847  addsubeq4  7848  muladd  8013  ltleadd  8075  reapmul1  8223  apreim  8231  receuap  8291  p1le  8465  lemul12b  8477  lbinf  8564  zdiv  8991  fzind  9018  fnn0ind  9019  uzss  9196  qmulcl  9279  qreccl  9284  xrlttr  9422  xaddass  9493  icc0r  9550  iooshf  9576  elfz5  9639  elfz0fzfz0  9744  fzind2  9857  ioo0  9878  ico0  9880  ioc0  9881  expnegap0  10142  expineg2  10143  mulexpzap  10174  expsubap  10182  expnbnd  10256  facndiv  10326  bccmpl  10341  bcval5  10350  bcpasc  10353  crim  10471  climshftlemg  10910  2sumeq2dv  10979  hash2iun  11087  dvdsval3  11292  dvdsnegb  11305  muldvds1  11313  muldvds2  11314  dvdscmul  11315  dvdsmulc  11316  dvds2ln  11321  divalgb  11417  ndvdssub  11422  gcddiv  11500  rpexp1i  11625  phiprmpw  11690  hashgcdeq  11696  innei  12114  iscnp4  12168  cnpnei  12169  cnnei  12182  cnconst  12184  ismeti  12274  isxmet2d  12276  elbl2ps  12320  elbl2  12321  xblpnfps  12326  xblpnf  12327  xblm  12345  blininf  12352  blssexps  12357  blssex  12358  blsscls2  12421  metss  12422  metrest  12434  metcn  12438  cdivcncfap  12499