Theorem 3expa 1206

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

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

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 983

This theorem is referenced by:  ad4ant123  1218  ad4ant124  1219  ad4ant134  1220  ad4ant234  1221  ad5ant123  1242  3anidm23  1310  mp3an2  1338  mpd3an3  1351  rgen3  2595  moi2  2961  sbc3ie  3079  2if2dc  3619  preq12bg  3827  issod  4384  wepo  4424  reuhypd  4536  funimass4  5652  fvtp1g  5815  f1imass  5866  fcof1o  5881  f1ofveu  5955  f1ocnvfv3  5956  acexmid  5966  2ndrn  6292  frecrdg  6517  oawordriexmid  6579  mapxpen  6970  findcard  7011  findcard2  7012  findcard2s  7013  ltapig  7486  ltanqi  7550  ltmnqi  7551  lt2addnq  7552  lt2mulnq  7553  prarloclemcalc  7650  genpassl  7672  genpassu  7673  prmuloc  7714  ltexprlemm  7748  ltexprlemfl  7757  ltexprlemfu  7759  lteupri  7765  ltaprg  7767  mul4  8239  add4  8268  cnegexlem2  8283  cnegexlem3  8284  2addsub  8321  addsubeq4  8322  muladd  8491  ltleadd  8554  reapmul1  8703  apreim  8711  receuap  8777  p1le  8957  lemul12b  8969  lbinf  9056  zdiv  9496  fzind  9523  fnn0ind  9524  uzss  9704  qmulcl  9793  qreccl  9798  xrlttr  9952  xaddass  10026  icc0r  10083  iooshf  10109  elfz5  10174  elfz0fzfz0  10283  fzind2  10405  ioo0  10439  ico0  10441  ioc0  10442  expnegap0  10729  expineg2  10730  mulexpzap  10761  expsubap  10769  expnbnd  10845  facndiv  10921  bccmpl  10936  bcval5  10945  bcpasc  10948  ccatrn  11103  swrdspsleq  11158  swrdccat2  11162  ccatpfx  11192  pfxccat1  11193  swrdswrd  11196  cats1un  11212  crim  11284  climshftlemg  11728  2sumeq2dv  11797  hash2iun  11905  2cprodeq2dv  11994  dvdsval3  12217  dvdsnegb  12234  muldvds1  12242  muldvds2  12243  dvdscmul  12244  dvdsmulc  12245  dvds2ln  12250  divalgb  12351  ndvdssub  12356  gcddiv  12455  rpexp1i  12591  phiprmpw  12659  hashgcdeq  12677  pythagtriplem1  12703  pockthg  12795  infpnlem1  12797  4sqlem3  12828  imasaddfnlemg  13261  mndpfo  13385  grplmulf1o  13521  grplactcnv  13549  mulgnn0subcl  13586  mulgsubcl  13587  mulgdir  13605  issubg2m  13640  issubgrpd2  13641  nmzsubg  13661  eqgen  13678  ghmmulg  13707  ghmf1  13724  kerf1ghm  13725  conjghm  13727  srglmhm  13870  srgrmhm  13871  ringlghm  13938  ringrghm  13939  oppr1g  13959  dvdsrcl2  13976  crngunit  13988  subsubrng  14091  subrgugrp  14117  subsubrg  14122  islmod  14168  lmodvsdir  14189  lmodvsass  14190  lsssubg  14254  lss1d  14260  lidlsubg  14363  lidlsubcl  14364  expghmap  14484  mulgghm2  14485  innei  14750  iscnp4  14805  cnpnei  14806  cnnei  14819  cnconst  14821  ismeti  14933  isxmet2d  14935  elbl2ps  14979  elbl2  14980  xblpnfps  14985  xblpnf  14986  xblm  15004  blininf  15011  blssexps  15016  blssex  15017  blsscls2  15080  metss  15081  metrest  15093  metcn  15101  divcnap  15152  cdivcncfap  15191  dvply1  15352  lgslem4  15595  lgscllem  15599  lgsneg1  15617  lgsne0  15630