Theorem 3expa 1265

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3anidm23  1385  mp3an2  1412  mpd3an3  1425  rgen3  2976  moi2  3387  sbc3ie  3507  2if2  4136  preq12bg  4386  prel12g  4387  ralxfrd2  4884  reuhypd  4895  otsndisj  4979  funcnvqp  5952  fvtp1g  6463  fntpb  6473  f1imass  6521  weisoeq  6605  f1ofveu  6645  f1ocnvfv3  6646  curry1f  7271  curry2f  7273  funsssuppss  7321  tfrlem11  7484  oalimcl  7640  oeordsuc  7674  oelim2  7675  nneob  7732  mapxpen  8126  findcard  8199  wemaplem3  8453  en2eqpr  8830  infxpabs  9034  infxp  9037  cfflb  9081  cfsmolem  9092  isf32lem12  9186  fin1a2lem9  9230  fin1a2s  9236  axcc3  9260  axdc3lem4  9275  zornn0g  9327  pwfseqlem4  9484  tskwun  9606  tskint  9607  tskxp  9609  tskmap  9610  gruf  9633  gruwun  9635  grutsk1  9643  addcanpi  9721  ltapi  9725  mul4  10205  add4  10256  2addsub  10295  addsubeq4  10296  muladd  10462  ltleadd  10511  receu  10672  p1le  10866  lemul12b  10880  lbinf  10976  zdiv  11447  fzind  11475  fnn0ind  11476  uzss  11708  zbtwnre  11786  qmulcl  11806  qreccl  11808  xrlttr  11973  xaddass  12079  xmulasslem3  12116  xmulass  12117  xadddilem  12124  xrsupsslem  12137  xrinfmsslem  12138  supxrunb1  12149  ixxin  12192  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  iooshf  12252  prunioo  12301  ioojoin  12303  elfz5  12334  elfz0fzfz0  12444  elfzonelfzo  12570  fzind2  12586  mulexpz  12900  expsub  12908  digit2  12997  digit1  12998  facndiv  13075  faclbnd4lem4  13083  faclbnd4  13084  faclbnd5  13085  bccmpl  13096  bcval5  13105  bcpasc  13108  hashunx  13175  hashdmpropge2  13265  ccatrn  13372  swrdccat1  13457  swrdccat2  13458  swrdswrd  13460  cats1un  13475  cshf1  13556  crim  13855  absmax  14069  ello12r  14248  elo12r  14259  climshftlem  14305  2sumeq2dv  14436  hash2iun  14555  expcnv  14596  2cprodeq2dv  14655  rpnnen2lem7  14949  dvdsval3  14987  dvdsnegb  14999  muldvds1  15006  muldvds2  15007  dvdscmul  15008  dvdsmulc  15009  dvdsmulcr  15011  dvds2ln  15014  divalgb  15127  ndvdssub  15133  gcddiv  15268  lcmfval  15334  lcmfcl  15341  dvdslcmf  15344  rpexp1i  15433  phiprmpw  15481  hashgcdeq  15494  pythagtriplem1  15521  pockthg  15610  infpnlem1  15614  4sqlem3  15654  0ramcl  15727  firest  16093  imasaddfnlem  16188  imasleval  16201  xpsfrn2  16230  mrerintcl  16257  iscatd  16334  fullestrcsetc  16791  fullsetcestrc  16806  clatleglb  17126  mreclatBAD  17187  pslem  17206  mrcmndind  17366  grplmulf1o  17489  grplactcnv  17518  mulgnn0subcl  17554  mulgsubcl  17555  mulgdir  17573  issubg2  17609  issubgrpd2  17610  cycsubgcl  17620  cycsubgss  17621  nmzsubg  17635  eqgen  17647  ghmmulg  17672  conjghm  17691  symgfixfo  17859  odeq  17969  odval2  17970  odf1  17979  dfod2  17981  gexdvds  17999  gexdvds2  18000  gexcl2  18004  gexdvds3  18005  sylow2blem2  18036  efgsp1  18150  efgrelexlemb  18163  mulgmhm  18233  mulgghm  18234  iscyggen2  18283  iscyg3  18288  srglmhm  18535  srgrmhm  18536  ringlghm  18604  ringrghm  18605  gsumdixp  18609  dvdsrcl2  18650  crngunit  18662  kerf1hrm  18743  subrgugrp  18799  cntzsubr  18812  lmodvsdir  18887  lmodvsass  18888  lmodvsghm  18924  lsssubg  18957  lss1d  18963  islbs2  19154  lidlsubg  19215  lidlsubcl  19216  quscrng  19240  lpigen  19256  xrsdsreval  19791  expghm  19844  mulgghm2  19845  ip0r  19982  obs2ss  20073  islindf3  20165  scmatscm  20319  scmataddcl  20322  scmatsubcl  20323  scmatfo  20336  matunit  20484  cpmatelimp  20517  cpmatelimp2  20519  cpmatinvcl  20522  cpmatmcl  20524  mat2pmatf  20533  m2cpmf  20547  cpm2mf  20557  m2cpmfo  20561  m2cpminv  20565  decpmataa0  20573  pm2mpf  20603  pm2mpf1  20604  idpm2idmp  20606  pm2mpfo  20619  elcls2  20878  opnnei  20924  innei  20929  iscnp4  21067  cnpnei  21068  iscncl  21073  cnnei  21086  cnconst  21088  ordthauslem  21187  bwth  21213  1stccnp  21265  llyrest  21288  nllyrest  21289  kgenss  21346  xkoccn  21422  kqsat  21534  kqt0lem  21539  isr0  21540  fbssfi  21641  isfild  21662  filconn  21687  trfilss  21693  fgtr  21694  ufileu  21723  ufilen  21734  fmfnfmlem4  21761  fmfnfm  21762  hausflimi  21784  cnpflf2  21804  cnpflf  21805  cnflf  21806  cnpfcf  21845  cnfcf  21846  cnextcn  21871  tmdmulg  21896  clsnsg  21913  tsmsxplem1  21956  tsmsxp  21958  ustuqtop0  22044  ismeti  22130  isxmet2d  22132  elbl2ps  22194  elbl2  22195  xblpnfps  22200  xblpnf  22201  xbln0  22219  blin  22226  blssexps  22231  blssex  22232  blsscls2  22309  blcls  22311  blsscls  22312  metss  22313  metrest  22329  metcn  22348  metustbl  22371  psmetutop  22372  nmf2  22397  ngpi  22432  tngngp3  22460  nmdvr  22474  nmoi  22532  nmoix  22533  nmoleub  22535  nghmcn  22549  xrsxmet  22612  iccntr  22624  metdsle  22655  icoopnst  22738  iocopnst  22739  icccvx  22749  pi1xfr  22855  isclmi0  22898  iscvsi  22929  cphipval  23042  lmmbr  23056  lmmbr2  23057  iscfil3  23071  iscau2  23075  cfilres  23094  bcthlem1  23121  bcthlem4  23124  bcthlem5  23125  rrxmet  23191  ioombl  23333  iccvolcl  23335  ioovolcl  23338  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  ig1pcl  23935  ig1prsp  23937  aannenlem1  24083  taylplem1  24117  dvtaylp  24124  relogeftb  24331  logdivlt  24367  cxpexp  24414  rpcxpcl  24422  isppw2  24841  vmappw  24842  lgslem4  25025  lgscllem  25029  lgsneg1  25047  lgsne0  25060  cgraswap  25712  brbtwn2  25785  ax5seglem1  25808  ax5seglem2  25809  axcontlem4  25847  ewlkprop  26499  uspgr2wlkeq  26542  uhgrwkspthlem2  26650  eupth2lem3lem7  27094  frgr3vlem2  27138  3cyclfrgrrn1  27149  4cycl2vnunb  27154  frgrncvvdeqlem8  27170  grpoidinvlem3  27360  isvciOLD  27435  nmcvcn  27550  ipval2lem2  27559  sspimsval  27593  isblo2  27638  nmoo0  27646  blocni  27660  isph  27677  sspph  27710  hvadd4  27893  hiassdi  27948  ocsh  28142  chj4  28394  spansncol  28427  pjjsi  28559  hoscl  28604  hodcl  28606  hoadd4  28643  homco1  28660  homulass  28661  hoadddi  28662  hoadddir  28663  unoplin  28779  adjvalval  28796  hmoplin  28801  bralnfn  28807  brafnmul  28810  lnopmi  28859  lnopcoi  28862  hmops  28879  hmopm  28880  nmophmi  28890  lnfncnbd  28916  cnlnadjlem2  28927  adjlnop  28945  adjmul  28951  adjadd  28952  branmfn  28964  kbass5  28979  kbass6  28980  leop2  28983  leopadd  28991  leopmuli  28992  pjimai  29035  atcvatlem  29244  chirredlem2  29250  mdsymlem3  29264  mdsymlem5  29266  sumdmdii  29274  sumdmdlem  29277  cdj3lem2a  29295  cdj3lem2b  29296  cdj3lem3a  29298  cdj3i  29300  xreceu  29630  toslublem  29667  tosglblem  29669  ogrpaddltbi  29719  archiabllem1b  29746  archiabllem2c  29749  archiabl  29752  slmdvsdir  29769  slmdvsass  29770  pstmxmet  29940  ordtconnlem1  29970  hasheuni  30147  omsf  30358  ballotlemirc  30593  signswmnd  30634  bnj1204  31080  txpconn  31214  cvmscld  31255  elmpps  31470  dfrdg2  31701  wsuclem  31773  wsuclemOLD  31774  nosepdm  31834  segconeu  32118  linecom  32257  linethru  32260  lineintmo  32264  fnemeet2  32362  fnejoin2  32364  lindsdom  33403  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  heicant  33444  mblfinlem1  33446  mblfinlem3  33448  ismblfin  33450  cnambfre  33458  itg2addnclem2  33462  ftc1anclem1  33485  ftc1anclem5  33489  ftc1anclem6  33490  ftc2nc  33494  areacirclem2  33501  areacirclem4  33503  areacirclem5  33504  areacirc  33505  fzmul  33537  subspopn  33548  isbndx  33581  isbnd2  33582  isbnd3  33583  ssbnd  33587  prdstotbnd  33593  heibor1  33609  rrnmet  33628  rngonegmn1l  33740  rngohomco  33773  rngoisocnv  33780  rngoisoco  33781  crngohomfo  33805  isidlc  33814  rngoidl  33823  prnc  33866  ispridlc  33869  cvrval2  34561  glbconxN  34664  hlrelat5N  34687  cvratlem  34707  cvrat2  34715  athgt  34742  3dim2  34754  llnn0  34802  lplnn0N  34833  lvoln0N  34877  snatpsubN  35036  paddasslem18  35123  pmod1i  35134  lhpexle2  35296  lhpexle3lem  35297  lhpexle3  35298  ldilcnv  35401  trlcnv  35452  trlnidatb  35464  cdleme32snaw  35723  cdleme32fvaw  35727  cdleme42ke  35773  cdlemeg46gf  35821  cdleme50trn12  35840  cdlemg1cex  35876  cdlemb3  35894  tgrpgrplem  36037  tgrpabl  36039  tendoplcl2  36066  tendo0pl  36079  tendoicl  36084  tendoipl  36085  cdlemkid3N  36221  tendoex  36263  erngdvlem4  36279  erngdvlem4-rN  36287  dib1dim  36454  dib1dim2  36457  dihglbcpreN  36589  dihmeetALTN  36616  dih1dimatlem  36618  dihatlat  36623  oddcomabszz  37509  acongtr  37545  rpnnen3lem  37598  islssfg  37640  lmhmfgsplit  37656  unxpwdom3  37665  hbtlem7  37695  sdrgacs  37771  iocmbl  37798  ss2iundf  37951  nzss  38516  dvconstbi  38533  bccbc  38544  uzmptshftfval  38545  iccdifprioo  39742  climisp  39978  limsupresxr  39998  liminfresxr  39999  dvnmul  40158  volico  40200  volioore  40207  fourierdlem74  40397  fourierdlem75  40398  sge0iunmptlemfi  40630  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0xp  40646  hspmbllem2  40841  smflimlem3  40981  smfsupmpt  41021  smfinflem  41023  smfinfmpt  41025  smflimsupmpt  41035  smfliminfmpt  41038  pfxccat1  41410  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  sprsymrelfo  41747  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  rhmsubcrngclem2  42028  lcoss  42225  snlindsntorlem  42259  aacllem  42547