Theorem 3expa 1229

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

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

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 1006

This theorem is referenced by:  ad4ant123  1241  ad4ant124  1242  ad4ant134  1243  ad4ant234  1244  ad5ant123  1265  3anidm23  1333  mp3an2  1361  mpd3an3  1374  rgen3  2619  moi2  2987  sbc3ie  3105  2if2dc  3645  preq12bg  3856  issod  4416  wepo  4456  reuhypd  4568  funimass4  5696  fvtp1g  5862  f1imass  5915  fcof1o  5930  f1ofveu  6006  f1ocnvfv3  6007  acexmid  6017  2ndrn  6346  frecrdg  6574  oawordriexmid  6638  mapxpen  7034  findcard  7077  findcard2  7078  findcard2s  7079  ltapig  7558  ltanqi  7622  ltmnqi  7623  lt2addnq  7624  lt2mulnq  7625  prarloclemcalc  7722  genpassl  7744  genpassu  7745  prmuloc  7786  ltexprlemm  7820  ltexprlemfl  7829  ltexprlemfu  7831  lteupri  7837  ltaprg  7839  mul4  8311  add4  8340  cnegexlem2  8355  cnegexlem3  8356  2addsub  8393  addsubeq4  8394  muladd  8563  ltleadd  8626  reapmul1  8775  apreim  8783  receuap  8849  p1le  9029  lemul12b  9041  lbinf  9128  zdiv  9568  fzind  9595  fnn0ind  9596  uzss  9777  qmulcl  9871  qreccl  9876  xrlttr  10030  xaddass  10104  icc0r  10161  iooshf  10187  elfz5  10252  elfz0fzfz0  10361  fzind2  10486  ioo0  10520  ico0  10522  ioc0  10523  expnegap0  10810  expineg2  10811  mulexpzap  10842  expsubap  10850  expnbnd  10926  facndiv  11002  bccmpl  11017  bcval5  11026  bcpasc  11029  ccatrn  11190  swrdspsleq  11252  swrdccat2  11256  ccatpfx  11286  pfxccat1  11287  swrdswrd  11290  cats1un  11306  crim  11436  climshftlemg  11880  2sumeq2dv  11949  hash2iun  12058  2cprodeq2dv  12147  dvdsval3  12370  dvdsnegb  12387  muldvds1  12395  muldvds2  12396  dvdscmul  12397  dvdsmulc  12398  dvds2ln  12403  divalgb  12504  ndvdssub  12509  gcddiv  12608  rpexp1i  12744  phiprmpw  12812  hashgcdeq  12830  pythagtriplem1  12856  pockthg  12948  infpnlem1  12950  4sqlem3  12981  imasaddfnlemg  13415  mndpfo  13539  grplmulf1o  13675  grplactcnv  13703  mulgnn0subcl  13740  mulgsubcl  13741  mulgdir  13759  issubg2m  13794  issubgrpd2  13795  nmzsubg  13815  eqgen  13832  ghmmulg  13861  ghmf1  13878  kerf1ghm  13879  conjghm  13881  srglmhm  14025  srgrmhm  14026  ringlghm  14093  ringrghm  14094  oppr1g  14114  dvdsrcl2  14132  crngunit  14144  subsubrng  14247  subrgugrp  14273  subsubrg  14278  islmod  14324  lmodvsdir  14345  lmodvsass  14346  lsssubg  14410  lss1d  14416  lidlsubg  14519  lidlsubcl  14520  expghmap  14640  mulgghm2  14641  innei  14906  iscnp4  14961  cnpnei  14962  cnnei  14975  cnconst  14977  ismeti  15089  isxmet2d  15091  elbl2ps  15135  elbl2  15136  xblpnfps  15141  xblpnf  15142  xblm  15160  blininf  15167  blssexps  15172  blssex  15173  blsscls2  15236  metss  15237  metrest  15249  metcn  15257  divcnap  15308  cdivcncfap  15347  dvply1  15508  lgslem4  15751  lgscllem  15755  lgsneg1  15773  lgsne0  15786  uspgr2wlkeq  16235  eupth2lem3lem7fi  16344