Theorem 3expa 1257

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anidm23  1377  mp3an2  1404  mpd3an3  1417  rgen3  2959  moi2  3354  sbc3ie  3474  2if2  4086  preq12bg  4326  prel12g  4327  ralxfrd2  4810  reuhypd  4821  otsndisj  4904  funcnvqp  5866  fvtp1g  6368  fntpb  6378  f1imass  6422  weisoeq  6505  f1ofveu  6544  f1ocnvfv3  6545  curry1f  7158  curry2f  7160  funsssuppss  7208  tfrlem11  7371  oalimcl  7527  oeordsuc  7561  oelim2  7562  nneob  7619  mapxpen  8011  findcard  8084  wemaplem3  8336  en2eqpr  8713  infxpabs  8917  infxp  8920  cfflb  8964  cfsmolem  8975  isf32lem12  9069  fin1a2lem9  9113  fin1a2s  9119  axcc3  9143  axdc3lem4  9158  zornn0g  9210  pwfseqlem4  9363  tskwun  9485  tskint  9486  tskxp  9488  tskmap  9489  gruf  9512  gruwun  9514  grutsk1  9522  addcanpi  9600  ltapi  9604  mul4  10084  add4  10135  2addsub  10174  addsubeq4  10175  muladd  10341  ltleadd  10390  receu  10551  p1le  10745  lemul12b  10759  lbinf  10855  zdiv  11323  fzind  11351  fnn0ind  11352  uzss  11584  zbtwnre  11662  qmulcl  11682  qreccl  11684  xrlttr  11849  xaddass  11951  xmulasslem3  11988  xmulass  11989  xadddilem  11996  xrsupsslem  12009  xrinfmsslem  12010  supxrunb1  12021  ixxin  12063  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  iooshf  12123  prunioo  12172  ioojoin  12174  elfz5  12205  elfz0fzfz0  12313  elfzonelfzo  12436  fzind2  12448  mulexpz  12762  expsub  12770  digit2  12859  digit1  12860  facndiv  12937  faclbnd4lem4  12945  faclbnd4  12946  faclbnd5  12947  bccmpl  12958  bcval5  12967  bcpasc  12970  hashunx  13036  ccatrn  13225  swrdccat1  13309  swrdccat2  13310  swrdswrd  13312  cats1un  13327  cshf1  13407  crim  13703  absmax  13917  ello12r  14096  elo12r  14107  climshftlem  14153  2sumeq2dv  14283  expcnv  14435  2cprodeq2dv  14494  rpnnen2lem7  14788  dvdsval3  14825  dvdsnegb  14837  muldvds1  14844  muldvds2  14845  dvdscmul  14846  dvdsmulc  14847  dvdsmulcr  14849  dvds2ln  14852  divalgb  14965  ndvdssub  14971  gcddiv  15106  lcmfval  15172  lcmfcl  15179  dvdslcmf  15182  rpexp1i  15271  phiprmpw  15319  hashgcdeq  15332  pythagtriplem1  15359  pockthg  15448  infpnlem1  15452  4sqlem3  15492  0ramcl  15565  firest  15916  imasaddfnlem  16011  imasleval  16024  xpsfrn2  16053  mrerintcl  16080  iscatd  16157  fullestrcsetc  16614  fullsetcestrc  16629  clatleglb  16949  mreclatBAD  17010  pslem  17029  mrcmndind  17189  grplmulf1o  17312  grplactcnv  17341  mulgnn0subcl  17377  mulgsubcl  17378  mulgdir  17396  issubg2  17432  issubgrpd2  17433  cycsubgcl  17443  cycsubgss  17444  nmzsubg  17458  eqgen  17470  ghmmulg  17495  conjghm  17514  symgfixfo  17682  odeq  17792  odval2  17793  odf1  17802  dfod2  17804  gexdvds  17822  gexdvds2  17823  gexcl2  17827  gexdvds3  17828  sylow2blem2  17859  efgsp1  17973  efgrelexlemb  17986  mulgmhm  18056  mulgghm  18057  iscyggen2  18106  iscyg3  18111  srglmhm  18358  srgrmhm  18359  ringlghm  18427  ringrghm  18428  gsumdixp  18432  dvdsrcl2  18473  crngunit  18485  kerf1hrm  18566  subrgugrp  18622  cntzsubr  18635  lmodvsdir  18710  lmodvsass  18711  lmodvsghm  18747  lsssubg  18778  lss1d  18784  islbs2  18975  lidlsubg  19036  lidlsubcl  19037  quscrng  19061  lpigen  19077  xrsdsreval  19610  expghm  19663  mulgghm2  19664  ip0r  19801  obs2ss  19892  islindf3  19984  scmatscm  20138  scmataddcl  20141  scmatsubcl  20142  scmatfo  20155  matunit  20303  cpmatelimp  20336  cpmatelimp2  20338  cpmatinvcl  20341  cpmatmcl  20343  mat2pmatf  20352  m2cpmf  20366  cpm2mf  20376  m2cpmfo  20380  m2cpminv  20384  decpmataa0  20392  pm2mpf  20422  pm2mpf1  20423  idpm2idmp  20425  pm2mpfo  20438  elcls2  20688  opnnei  20734  innei  20739  iscnp4  20877  cnpnei  20878  iscncl  20883  cnnei  20896  cnconst  20898  ordthauslem  20997  bwth  21023  1stccnp  21075  llyrest  21098  nllyrest  21099  kgenss  21156  xkoccn  21232  kqsat  21344  kqt0lem  21349  isr0  21350  fbssfi  21451  isfild  21472  filcon  21497  trfilss  21503  fgtr  21504  ufileu  21533  ufilen  21544  fmfnfmlem4  21571  fmfnfm  21572  hausflimi  21594  cnpflf2  21614  cnpflf  21615  cnflf  21616  cnpfcf  21655  cnfcf  21656  cnextcn  21681  tmdmulg  21706  clsnsg  21723  tsmsxplem1  21766  tsmsxp  21768  ustuqtop0  21854  ismeti  21940  isxmet2d  21942  elbl2ps  22004  elbl2  22005  xblpnfps  22010  xblpnf  22011  xbln0  22029  blin  22036  blssexps  22041  blssex  22042  blsscls2  22119  blcls  22121  blsscls  22122  metss  22123  metrest  22139  metcn  22158  metustbl  22181  psmetutop  22182  nmf2  22207  ngpi  22242  tngngp3  22270  nmdvr  22284  nmoi  22342  nmoix  22343  nmoleub  22345  nghmcn  22359  xrsxmet  22420  iccntr  22432  metdsle  22463  icoopnst  22546  iocopnst  22547  icccvx  22557  pi1xfr  22663  isclmi0  22706  iscvsi  22737  cphipval  22850  lmmbr  22864  lmmbr2  22865  iscfil3  22879  iscau2  22883  cfilres  22902  bcthlem1  22929  bcthlem4  22932  bcthlem5  22933  rrxmet  22999  ioombl  23140  iccvolcl  23142  ioovolcl  23144  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  ig1pcl  23739  ig1prsp  23741  aannenlem1  23887  taylplem1  23921  dvtaylp  23928  relogeftb  24135  logdivlt  24171  cxpexp  24214  rpcxpcl  24222  isppw2  24641  vmappw  24642  lgslem4  24825  lgscllem  24829  lgsneg1  24847  lgsne0  24860  cgraswap  25512  brbtwn2  25585  ax5seglem1  25608  ax5seglem2  25609  axcontlem4  25647  nbgraf1olem5  25974  constr3cycl  26189  wwlknimp  26215  usg2wlkeq  26236  wwlknred  26251  wwlknext  26252  clwwlknprop  26300  3cyclfrgrarn1  26539  3cyclfrgrarn  26540  4cycl2vnunb  26544  frgrancvvdeqlemB  26565  usgreghash2spotv  26593  2spotmdisj  26595  grpoidinvlem3  26744  isvciOLD  26819  nmcvcn  26934  ipval2lem2  26943  sspimsval  26977  isblo2  27022  nmoo0  27030  blocni  27044  isph  27061  sspph  27094  hvadd4  27277  hiassdi  27332  ocsh  27526  chj4  27778  spansncol  27811  pjjsi  27943  hoscl  27988  hodcl  27990  hoadd4  28027  homco1  28044  homulass  28045  hoadddi  28046  hoadddir  28047  unoplin  28163  adjvalval  28180  hmoplin  28185  bralnfn  28191  brafnmul  28194  lnopmi  28243  lnopcoi  28246  hmops  28263  hmopm  28264  nmophmi  28274  lnfncnbd  28300  cnlnadjlem2  28311  adjlnop  28329  adjmul  28335  adjadd  28336  branmfn  28348  kbass5  28363  kbass6  28364  leop2  28367  leopadd  28375  leopmuli  28376  pjimai  28419  atcvatlem  28628  chirredlem2  28634  mdsymlem3  28648  mdsymlem5  28650  sumdmdii  28658  sumdmdlem  28661  cdj3lem2a  28679  cdj3lem2b  28680  cdj3lem3a  28682  cdj3i  28684  xreceu  28961  toslublem  28998  tosglblem  29000  ogrpaddltbi  29050  archiabllem1b  29077  archiabllem2c  29080  archiabl  29083  slmdvsdir  29100  slmdvsass  29101  pstmxmet  29268  ordtconlem1  29298  hasheuni  29474  omsf  29685  ballotlemirc  29920  signswmnd  29960  bnj1204  30334  txpcon  30468  cvmscld  30509  elmpps  30724  dfrdg2  30945  wsuclem  31017  wsuclemOLD  31018  nobndlem8  31098  segconeu  31288  linecom  31427  linethru  31430  lineintmo  31434  fnemeet2  31532  fnejoin2  31534  lindsdom  32573  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  heicant  32614  mblfinlem1  32616  mblfinlem3  32618  ismblfin  32620  cnambfre  32628  itg2addnclem2  32632  ftc1anclem1  32655  ftc1anclem5  32659  ftc1anclem6  32660  ftc2nc  32664  areacirclem2  32671  areacirclem4  32673  areacirclem5  32674  areacirc  32675  fzmul  32707  subspopn  32718  isbndx  32751  isbnd2  32752  isbnd3  32753  ssbnd  32757  prdstotbnd  32763  heibor1  32779  rrnmet  32798  rngonegmn1l  32910  rngohomco  32943  rngoisocnv  32950  rngoisoco  32951  crngohomfo  32975  isidlc  32984  rngoidl  32993  prnc  33036  ispridlc  33039  cvrval2  33579  glbconxN  33682  hlrelat5N  33705  cvratlem  33725  cvrat2  33733  athgt  33760  3dim2  33772  llnn0  33820  lplnn0N  33851  lvoln0N  33895  snatpsubN  34054  paddasslem18  34141  pmod1i  34152  lhpexle2  34314  lhpexle3lem  34315  lhpexle3  34316  ldilcnv  34419  trlcnv  34470  trlnidatb  34482  cdleme32snaw  34741  cdleme32fvaw  34745  cdleme42ke  34791  cdlemeg46gf  34839  cdleme50trn12  34858  cdlemg1cex  34894  cdlemb3  34912  tgrpgrplem  35055  tgrpabl  35057  tendoplcl2  35084  tendo0pl  35097  tendoicl  35102  tendoipl  35103  cdlemkid3N  35239  tendoex  35281  erngdvlem4  35297  erngdvlem4-rN  35305  dib1dim  35472  dib1dim2  35475  dihglbcpreN  35607  dihmeetALTN  35634  dih1dimatlem  35636  dihatlat  35641  oddcomabszz  36527  acongtr  36563  rpnnen3lem  36616  islssfg  36658  lmhmfgsplit  36674  unxpwdom3  36683  hbtlem7  36714  sdrgacs  36790  iocmbl  36817  ss2iundf  36970  nzss  37538  dvconstbi  37555  bccbc  37566  uzmptshftfval  37567  iccdifprioo  38589  dvnmul  38833  volico  38876  volioore  38883  fourierdlem74  39073  fourierdlem75  39074  issald  39227  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0xp  39322  hspmbllem2  39517  smflimlem3  39659  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  pfxccat1  40273  ewlkprop  40805  uspgr2wlkeq  40854  uhgr1wlkspthlem2  40960  eupth2lem3lem7  41402  frgr3vlem2  41444  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  frgrncvvdeqlemB  41477  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  rhmsubcrngclem2  41820  lcoss  42019  snlindsntorlem  42053  aacllem  42356