Theorem 3expa 1205

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

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

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 982

This theorem is referenced by:  ad4ant123  1217  ad4ant124  1218  ad4ant134  1219  ad4ant234  1220  ad5ant123  1241  3anidm23  1308  mp3an2  1336  mpd3an3  1349  rgen3  2577  moi2  2933  sbc3ie  3051  preq12bg  3788  issod  4337  wepo  4377  reuhypd  4489  funimass4  5587  fvtp1g  5745  f1imass  5796  fcof1o  5811  f1ofveu  5885  f1ocnvfv3  5886  acexmid  5896  2ndrn  6209  frecrdg  6434  oawordriexmid  6496  mapxpen  6877  findcard  6917  findcard2  6918  findcard2s  6919  ltapig  7368  ltanqi  7432  ltmnqi  7433  lt2addnq  7434  lt2mulnq  7435  prarloclemcalc  7532  genpassl  7554  genpassu  7555  prmuloc  7596  ltexprlemm  7630  ltexprlemfl  7639  ltexprlemfu  7641  lteupri  7647  ltaprg  7649  mul4  8120  add4  8149  cnegexlem2  8164  cnegexlem3  8165  2addsub  8202  addsubeq4  8203  muladd  8372  ltleadd  8434  reapmul1  8583  apreim  8591  receuap  8657  p1le  8837  lemul12b  8849  lbinf  8936  zdiv  9372  fzind  9399  fnn0ind  9400  uzss  9580  qmulcl  9669  qreccl  9674  xrlttr  9827  xaddass  9901  icc0r  9958  iooshf  9984  elfz5  10049  elfz0fzfz0  10158  fzind2  10271  ioo0  10292  ico0  10294  ioc0  10295  expnegap0  10562  expineg2  10563  mulexpzap  10594  expsubap  10602  expnbnd  10678  facndiv  10754  bccmpl  10769  bcval5  10778  bcpasc  10781  crim  10902  climshftlemg  11345  2sumeq2dv  11414  hash2iun  11522  2cprodeq2dv  11611  dvdsval3  11833  dvdsnegb  11850  muldvds1  11858  muldvds2  11859  dvdscmul  11860  dvdsmulc  11861  dvds2ln  11866  divalgb  11965  ndvdssub  11970  gcddiv  12055  rpexp1i  12189  phiprmpw  12257  hashgcdeq  12274  pythagtriplem1  12300  pockthg  12392  infpnlem1  12394  4sqlem3  12425  imasaddfnlemg  12794  mndpfo  12914  grplmulf1o  13033  grplactcnv  13061  mulgnn0subcl  13092  mulgsubcl  13093  mulgdir  13111  issubg2m  13145  issubgrpd2  13146  nmzsubg  13166  eqgen  13183  ghmmulg  13212  ghmf1  13229  kerf1ghm  13230  conjghm  13232  srglmhm  13364  srgrmhm  13365  oppr1g  13449  dvdsrcl2  13466  crngunit  13478  subsubrng  13578  subrgugrp  13604  subsubrg  13609  islmod  13624  lmodvsdir  13645  lmodvsass  13646  lsssubg  13710  lss1d  13716  lidlsubg  13819  lidlsubcl  13820  mulgghm2  13923  innei  14140  iscnp4  14195  cnpnei  14196  cnnei  14209  cnconst  14211  ismeti  14323  isxmet2d  14325  elbl2ps  14369  elbl2  14370  xblpnfps  14375  xblpnf  14376  xblm  14394  blininf  14401  blssexps  14406  blssex  14407  blsscls2  14470  metss  14471  metrest  14483  metcn  14491  divcnap  14532  cdivcncfap  14564  lgslem4  14882  lgscllem  14886  lgsneg1  14904  lgsne0  14917