Theorem 3expa 1230

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

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

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 1007

This theorem is referenced by:  ad4ant123  1242  ad4ant124  1243  ad4ant134  1244  ad4ant234  1245  ad5ant123  1266  3anidm23  1334  mp3an2  1362  mpd3an3  1375  rgen3  2629  moi2  2998  sbc3ie  3116  2if2dc  3662  preq12bg  3877  issod  4440  wepo  4480  reuhypd  4592  funimass4  5727  fvtp1g  5892  f1imass  5947  fcof1o  5962  f1ofveu  6038  f1ocnvfv3  6039  acexmid  6049  2ndrn  6377  funsssuppss  6458  frecrdg  6639  oawordriexmid  6703  mapxpen  7101  findcard  7145  findcard2  7146  findcard2s  7147  ltapig  7653  ltanqi  7717  ltmnqi  7718  lt2addnq  7719  lt2mulnq  7720  prarloclemcalc  7817  genpassl  7839  genpassu  7840  prmuloc  7881  ltexprlemm  7915  ltexprlemfl  7924  ltexprlemfu  7926  lteupri  7932  ltaprg  7934  mul4  8405  add4  8434  cnegexlem2  8449  cnegexlem3  8450  2addsub  8487  addsubeq4  8488  muladd  8657  ltleadd  8720  reapmul1  8869  apreim  8877  receuap  8943  p1le  9123  lemul12b  9135  lbinf  9222  zdiv  9666  fzind  9693  fnn0ind  9694  uzss  9875  qmulcl  9969  qreccl  9974  xrlttr  10128  xaddass  10202  icc0r  10259  iooshf  10285  elfz5  10351  elfz0fzfz0  10460  fzind2  10585  ioo0  10619  ico0  10621  ioc0  10622  expnegap0  10909  expineg2  10910  mulexpzap  10941  expsubap  10949  expnbnd  11025  facndiv  11101  bccmpl  11116  bcval5  11125  bcpasc  11128  ccatrn  11297  swrdspsleq  11359  swrdccat2  11363  ccatpfx  11393  pfxccat1  11394  swrdswrd  11397  cats1un  11413  crim  11543  climshftlemg  11987  2sumeq2dv  12056  hash2iun  12165  2cprodeq2dv  12254  dvdsval3  12477  dvdsnegb  12494  muldvds1  12502  muldvds2  12503  dvdscmul  12504  dvdsmulc  12505  dvds2ln  12510  divalgb  12611  ndvdssub  12616  gcddiv  12715  rpexp1i  12851  phiprmpw  12919  hashgcdeq  12937  pythagtriplem1  12963  pockthg  13055  infpnlem1  13057  4sqlem3  13088  imasaddfnlemg  13527  mndpfo  13651  grplmulf1o  13787  grplactcnv  13815  mulgnn0subcl  13852  mulgsubcl  13853  mulgdir  13871  issubg2m  13906  issubgrpd2  13907  nmzsubg  13927  eqgen  13944  ghmmulg  13973  ghmf1  13990  kerf1ghm  13991  conjghm  13993  srglmhm  14137  srgrmhm  14138  ringlghm  14205  ringrghm  14206  oppr1g  14226  dvdsrcl2  14244  crngunit  14256  subsubrng  14359  subrgugrp  14385  subsubrg  14390  islmod  14439  lmodvsdir  14460  lmodvsass  14461  lsssubg  14525  lss1d  14531  lidlsubg  14634  lidlsubcl  14635  expghmap  14755  mulgghm2  14756  innei  15028  iscnp4  15083  cnpnei  15084  cnnei  15097  cnconst  15099  ismeti  15211  isxmet2d  15213  elbl2ps  15257  elbl2  15258  xblpnfps  15263  xblpnf  15264  xblm  15282  blininf  15289  blssexps  15294  blssex  15295  blsscls2  15358  metss  15359  metrest  15371  metcn  15379  divcnap  15430  cdivcncfap  15469  dvply1  15630  lgslem4  15876  lgscllem  15880  lgsneg1  15898  lgsne0  15911  uspgr2wlkeq  16360  eupth2lem3lem7fi  16469