Theorem 3expa 1227

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

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

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 1004

This theorem is referenced by:  ad4ant123  1239  ad4ant124  1240  ad4ant134  1241  ad4ant234  1242  ad5ant123  1263  3anidm23  1331  mp3an2  1359  mpd3an3  1372  rgen3  2617  moi2  2984  sbc3ie  3102  2if2dc  3642  preq12bg  3851  issod  4410  wepo  4450  reuhypd  4562  funimass4  5686  fvtp1g  5851  f1imass  5904  fcof1o  5919  f1ofveu  5995  f1ocnvfv3  5996  acexmid  6006  2ndrn  6335  frecrdg  6560  oawordriexmid  6624  mapxpen  7017  findcard  7058  findcard2  7059  findcard2s  7060  ltapig  7536  ltanqi  7600  ltmnqi  7601  lt2addnq  7602  lt2mulnq  7603  prarloclemcalc  7700  genpassl  7722  genpassu  7723  prmuloc  7764  ltexprlemm  7798  ltexprlemfl  7807  ltexprlemfu  7809  lteupri  7815  ltaprg  7817  mul4  8289  add4  8318  cnegexlem2  8333  cnegexlem3  8334  2addsub  8371  addsubeq4  8372  muladd  8541  ltleadd  8604  reapmul1  8753  apreim  8761  receuap  8827  p1le  9007  lemul12b  9019  lbinf  9106  zdiv  9546  fzind  9573  fnn0ind  9574  uzss  9755  qmulcl  9844  qreccl  9849  xrlttr  10003  xaddass  10077  icc0r  10134  iooshf  10160  elfz5  10225  elfz0fzfz0  10334  fzind2  10457  ioo0  10491  ico0  10493  ioc0  10494  expnegap0  10781  expineg2  10782  mulexpzap  10813  expsubap  10821  expnbnd  10897  facndiv  10973  bccmpl  10988  bcval5  10997  bcpasc  11000  ccatrn  11157  swrdspsleq  11215  swrdccat2  11219  ccatpfx  11249  pfxccat1  11250  swrdswrd  11253  cats1un  11269  crim  11385  climshftlemg  11829  2sumeq2dv  11898  hash2iun  12006  2cprodeq2dv  12095  dvdsval3  12318  dvdsnegb  12335  muldvds1  12343  muldvds2  12344  dvdscmul  12345  dvdsmulc  12346  dvds2ln  12351  divalgb  12452  ndvdssub  12457  gcddiv  12556  rpexp1i  12692  phiprmpw  12760  hashgcdeq  12778  pythagtriplem1  12804  pockthg  12896  infpnlem1  12898  4sqlem3  12929  imasaddfnlemg  13363  mndpfo  13487  grplmulf1o  13623  grplactcnv  13651  mulgnn0subcl  13688  mulgsubcl  13689  mulgdir  13707  issubg2m  13742  issubgrpd2  13743  nmzsubg  13763  eqgen  13780  ghmmulg  13809  ghmf1  13826  kerf1ghm  13827  conjghm  13829  srglmhm  13972  srgrmhm  13973  ringlghm  14040  ringrghm  14041  oppr1g  14061  dvdsrcl2  14079  crngunit  14091  subsubrng  14194  subrgugrp  14220  subsubrg  14225  islmod  14271  lmodvsdir  14292  lmodvsass  14293  lsssubg  14357  lss1d  14363  lidlsubg  14466  lidlsubcl  14467  expghmap  14587  mulgghm2  14588  innei  14853  iscnp4  14908  cnpnei  14909  cnnei  14922  cnconst  14924  ismeti  15036  isxmet2d  15038  elbl2ps  15082  elbl2  15083  xblpnfps  15088  xblpnf  15089  xblm  15107  blininf  15114  blssexps  15119  blssex  15120  blsscls2  15183  metss  15184  metrest  15196  metcn  15204  divcnap  15255  cdivcncfap  15294  dvply1  15455  lgslem4  15698  lgscllem  15702  lgsneg1  15720  lgsne0  15733  uspgr2wlkeq  16111