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  2581  moi2  2942  sbc3ie  3060  preq12bg  3800  issod  4351  wepo  4391  reuhypd  4503  funimass4  5608  fvtp1g  5767  f1imass  5818  fcof1o  5833  f1ofveu  5907  f1ocnvfv3  5908  acexmid  5918  2ndrn  6238  frecrdg  6463  oawordriexmid  6525  mapxpen  6906  findcard  6946  findcard2  6947  findcard2s  6948  ltapig  7400  ltanqi  7464  ltmnqi  7465  lt2addnq  7466  lt2mulnq  7467  prarloclemcalc  7564  genpassl  7586  genpassu  7587  prmuloc  7628  ltexprlemm  7662  ltexprlemfl  7671  ltexprlemfu  7673  lteupri  7679  ltaprg  7681  mul4  8153  add4  8182  cnegexlem2  8197  cnegexlem3  8198  2addsub  8235  addsubeq4  8236  muladd  8405  ltleadd  8467  reapmul1  8616  apreim  8624  receuap  8690  p1le  8870  lemul12b  8882  lbinf  8969  zdiv  9408  fzind  9435  fnn0ind  9436  uzss  9616  qmulcl  9705  qreccl  9710  xrlttr  9864  xaddass  9938  icc0r  9995  iooshf  10021  elfz5  10086  elfz0fzfz0  10195  fzind2  10309  ioo0  10331  ico0  10333  ioc0  10334  expnegap0  10621  expineg2  10622  mulexpzap  10653  expsubap  10661  expnbnd  10737  facndiv  10813  bccmpl  10828  bcval5  10837  bcpasc  10840  crim  11005  climshftlemg  11448  2sumeq2dv  11517  hash2iun  11625  2cprodeq2dv  11714  dvdsval3  11937  dvdsnegb  11954  muldvds1  11962  muldvds2  11963  dvdscmul  11964  dvdsmulc  11965  dvds2ln  11970  divalgb  12069  ndvdssub  12074  gcddiv  12159  rpexp1i  12295  phiprmpw  12363  hashgcdeq  12380  pythagtriplem1  12406  pockthg  12498  infpnlem1  12500  4sqlem3  12531  imasaddfnlemg  12900  mndpfo  13022  grplmulf1o  13149  grplactcnv  13177  mulgnn0subcl  13208  mulgsubcl  13209  mulgdir  13227  issubg2m  13262  issubgrpd2  13263  nmzsubg  13283  eqgen  13300  ghmmulg  13329  ghmf1  13346  kerf1ghm  13347  conjghm  13349  srglmhm  13492  srgrmhm  13493  ringlghm  13560  ringrghm  13561  oppr1g  13581  dvdsrcl2  13598  crngunit  13610  subsubrng  13713  subrgugrp  13739  subsubrg  13744  islmod  13790  lmodvsdir  13811  lmodvsass  13812  lsssubg  13876  lss1d  13882  lidlsubg  13985  lidlsubcl  13986  expghmap  14106  mulgghm2  14107  innei  14342  iscnp4  14397  cnpnei  14398  cnnei  14411  cnconst  14413  ismeti  14525  isxmet2d  14527  elbl2ps  14571  elbl2  14572  xblpnfps  14577  xblpnf  14578  xblm  14596  blininf  14603  blssexps  14608  blssex  14609  blsscls2  14672  metss  14673  metrest  14685  metcn  14693  divcnap  14744  cdivcncfap  14783  dvply1  14943  lgslem4  15160  lgscllem  15164  lgsneg1  15182  lgsne0  15195