Theorem 3expb 1121

Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expb	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3expb

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 418	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3expia  1122  3adant3r1  1184  3adant3r2  1185  3adant3r3  1186  mp3an1  1451  sotri  6085  fnfco  6700  mpoeq3dva  7438  oprres  7529  fovcdmda  7532  fnmpoovd  8031  offval22  8032  bropfvvvvlem  8035  fnsuppres  8135  suppsssn  8145  sprmpod  8168  oaass  8490  omlimcl  8507  odi  8508  nnmsucr  8555  nnasmo  8593  unfi  9099  ttrclse  9642  cflim2  10179  mulcanenq  10877  mul4  11308  add4  11361  2addsub  11401  addsubeq4  11402  subadd4  11432  muladd  11576  ltleadd  11627  divmul  11806  divne0  11815  div23  11822  div12  11825  div11  11831  divsubdir  11842  subdivcomb1  11844  divcan5  11851  divmuleq  11854  divcan6  11856  divdiv32  11857  div2sub  11974  letrp1  11993  lemul12b  12006  lediv1  12015  lt2mul2div  12028  lemuldiv  12030  ltdiv2  12036  ledivdiv  12039  lediv2  12040  ltdiv23  12041  lediv23  12042  sup2  12106  cju  12149  nndivre  12212  nndivtr  12218  nn0addge1  12477  nn0addge2  12478  peano2uz2  12611  uzind  12615  uzind3  12617  fzind  12621  fnn0ind  12622  uzind4  12850  qre  12897  irrmul  12918  rpdivcl  12963  rerpdivcl  12968  xrinfmsslem  13254  ixxin  13309  iccshftr  13433  iccshftl  13435  iccdil  13437  icccntr  13439  fzaddel  13506  fzadd2  13507  fzrev  13535  modlt  13833  modcyc  13859  axdc4uzlem  13939  expdiv  14069  fundmge2nop0  14458  swrd00  14601  swrdcl  14602  swrdnnn0nd  14613  swrd0  14615  swrdwrdsymb  14619  ccatpfx  14657  swrdccat  14691  splid  14709  swrdco  14793  2shfti  15036  isermulc2  15614  fsummulc2  15740  dvdscmulr  16247  dvdsmulcr  16248  dvds2add  16253  dvds2sub  16254  dvdstr  16257  alzdvds  16283  divalg2  16368  dvdslegcd  16467  lcmgcdlem  16569  lcmgcdeq  16575  isprm6  16678  pcqcl  16821  vdwmc2  16944  ressinbas  17209  cicer  17767  isposd  18282  pleval2i  18294  poslubmo  18369  posglbmo  18370  tosso  18377  mgmplusf  18612  ismgmd  18614  grpinva  18636  idmgmhm  18663  resmgmhm  18673  resmgmhm2  18674  resmgmhm2b  18675  mgmhmco  18676  mgmhmima  18677  submgmacs  18679  sgrpidmnd  18701  ismndd  18718  imasmnd2  18736  idmhm  18757  mndvcl  18759  issubm2  18766  0mhm  18781  resmhm  18782  resmhm2  18783  resmhm2b  18784  mhmco  18785  mhmimalem  18786  submacs  18789  prdspjmhm  18791  pwsdiagmhm  18793  pwsco1mhm  18794  pwsco2mhm  18795  gsumwsubmcl  18799  gsumsgrpccat  18802  gsumwmhm  18807  grpinvcnv  18976  grpinvnzcl  18981  grpsubf  18989  imasgrp2  19025  qusgrp2  19028  mhmfmhm  19035  mulgnnsubcl  19056  mulgnndir  19073  issubg4  19115  isnsg3  19129  nsgacs  19131  nsgid  19139  qusadd  19157  qus0subgadd  19168  ghmmhm  19195  ghmmhmb  19196  idghm  19200  resghm  19201  ghmf1  19215  qusghm  19224  gaid  19268  subgga  19269  gasubg  19271  invoppggim  19329  gsmsymgrfix  19397  smndlsmidm  19625  pj1ghm  19672  mulgnn0di  19794  mulgmhm  19796  mulgghm  19797  ghmfghm  19799  invghm  19802  ghmplusg  19815  ablnsg  19816  qusabl  19834  gsumval3eu  19873  gsumval3  19876  gsumzcl2  19879  gsumzaddlem  19890  gsumzadd  19891  gsumzmhm  19906  gsumzoppg  19913  srgfcl  20171  srgcom4lem  20188  srgmulgass  20192  srglmhm  20196  srgrmhm  20197  ringcomlem  20254  ringlghm  20287  ringrghm  20288  pwspjmhmmgpd  20301  c0mgm  20433  c0mhm  20434  isnzr2  20489  subrngringnsg  20524  issubrng2  20529  rhmimasubrnglem  20536  issubrg2  20563  domnmuln0  20680  isdomn3  20686  issrngd  20826  islmodd  20855  lmodscaf  20873  lcomf  20890  lmodvsghm  20912  rmodislmodlem  20918  lssacs  20956  idlmhm  21031  invlmhm  21032  lmhmvsca  21035  reslmhm2  21043  reslmhm2b  21044  pwsdiaglmhm  21047  pwssplit2  21050  pwssplit3  21051  issubrgd  21179  qusrhm  21269  qusmul2idl  21272  crngridl  21273  qusmulrng  21275  expmhm  21429  zntoslem  21549  znfld  21553  psgnghm  21573  phlipf  21645  frlmup1  21791  asclghm  21875  asclrhm  21883  rnasclmulcl  21887  psraddcl  21931  psrvscacl  21943  psrass23  21960  psrbagev1  22068  coe1sclmulfv  22261  cply1mul  22274  evls1fpws  22347  rhmply1vsca  22366  matbas2d  22401  submaeval  22560  minmar1eval  22627  cpmatacl  22694  pmatcollpw1  22754  pmatcollpw  22759  tgclb  22948  topbas  22950  ntrss  23033  mretopd  23070  neissex  23105  cnpnei  23242  lmcnp  23282  ordthaus  23362  llynlly  23455  restnlly  23460  llyidm  23466  nllyidm  23467  ptbasin  23555  txcnp  23598  ist0-4  23707  kqt0lem  23714  isr0  23715  regr1lem2  23718  cmphmph  23766  connhmph  23767  fbun  23818  trfbas2  23821  isfil2  23834  isfild  23836  infil  23841  fbasfip  23846  fbasrn  23862  trfil2  23865  rnelfmlem  23930  fmfnfmlem3  23934  flimopn  23953  txflf  23984  fclsnei  23997  fclsfnflim  24005  fcfnei  24013  clssubg  24087  tgphaus  24095  qustgplem  24099  tsmsadd  24125  psmetxrge0  24291  psmetlecl  24293  xmetlecl  24324  xmettpos  24327  imasdsf1olem  24351  imasf1oxmet  24353  imasf1omet  24354  elbl3ps  24369  elbl3  24370  metss  24486  comet  24491  stdbdxmet  24493  stdbdmet  24494  methaus  24498  nrmmetd  24552  abvmet  24553  isngp4  24590  subgngp  24613  nmoi2  24708  nmoleub  24709  nmoid  24720  bl2ioo  24770  zcld  24792  divcn  24848  divccn  24853  cncfcdm  24878  divccncf  24886  icoopnst  24919  clmzlmvsca  25093  cph2ass  25193  tcphcph  25217  cfilfcls  25254  bcthlem2  25305  rrxmet  25388  rrxdstprj1  25389  rrxdsfi  25391  cldcss  25421  dvrec  25935  dvmptfsum  25955  aalioulem3  26314  taylply2  26347  taylply2OLD  26348  efsubm  26531  dchrelbasd  27219  dchrmulcl  27229  2sqreulem3  27433  pntrmax  27544  padicabv  27610  nosupbnd2  27697  noinfbnd2  27712  sltsd  27777  divmulsw  28202  axtgcont  28554  xmstrkgc  28971  axsegconlem1  29003  axlowdimlem15  29042  usgredg2vlem1  29311  usgredg2vlem2  29312  iswlkon  29742  wwlksnextsurj  29986  elwwlks2  30055  elwspths2spth  30056  frrusgrord  30429  numclwwlk1lem2foalem  30439  grpoidinvlem2  30594  grpoidinvlem3  30595  ablo4  30639  ablomuldiv  30641  nvaddsub4  30746  nvmeq0  30747  sspmval  30822  sspimsval  30827  lnosub  30848  dipsubdir  30937  hvadd4  31125  hvpncan  31128  his35  31177  hiassdi  31180  shscli  31406  shmodsi  31478  chj4  31624  spansnmul  31653  spansncol  31657  spanunsni  31668  hoadd4  31873  hosubadd4  31903  lnopl  32003  unopf1o  32005  counop  32010  lnfnl  32020  hmopadj2  32030  eighmre  32052  lnopmi  32089  lnophsi  32090  hmops  32109  hmopm  32110  cnlnadjlem2  32157  adjmul  32181  adjadd  32182  kbass6  32210  mdslj1i  32408  mdslj2i  32409  mdslmd1lem1  32414  mdslmd2i  32419  chirredlem3  32481  isoun  32793  xdivmul  33002  odutos  33046  lmodvslmhm  33129  isarchi2  33264  archiabllem2  33276  imasmhm  33432  imasghm  33433  imasrhm  33434  imaslmhm  33435  quslmhm  33437  tngdim  33776  fedgmullem2  33793  metider  34057  pl1cn  34118  rossros  34343  ismeas  34362  dya2iocnei  34445  inelcarsg  34474  signstfvc  34737  bnj563  34905  fisshasheq  35316  cnpconn  35431  cvmseu  35477  elmrsubrn  35721  mrsubco  35722  fneint  36549  fnessref  36558  tailfb  36578  onsucuni3  37700  pibt2  37750  ptrecube  37958  poimirlem4  37962  heicant  37993  mblfinlem1  37995  mblfinlem2  37996  mblfinlem3  37997  mblfinlem4  37998  cnambfre  38006  itg2addnclem2  38010  ftc1anclem5  38035  ftc1anclem6  38036  metf1o  38093  isbnd3b  38123  equivbnd  38128  heiborlem3  38151  rrnmet  38167  rrndstprj1  38168  rrntotbnd  38174  exidcl  38214  ghomco  38229  ghomdiv  38230  grpokerinj  38231  rngoneglmul  38281  rngonegrmul  38282  rngosubdi  38283  rngosubdir  38284  isdrngo2  38296  rngohomco  38312  rngoisocnv  38319  riscer  38326  crngm4  38341  crngohomfo  38344  idlsubcl  38361  inidl  38368  keridl  38370  ispridlc  38408  pridlc3  38411  dmncan1  38414  lflvscl  39540  3dim0  39920  linepsubN  40215  cdlemg2fvlem  41057  trlcoat  41186  istendod  41225  dva1dim  41448  dvhvaddcomN  41559  dihf11  41730  dihlatat  41800  sn-sup2  42953  fsuppssind  43043  mhphf  43047  ismrc  43150  isnacs3  43159  mzpindd  43195  pellex  43284  monotoddzzfi  43391  lermxnn0  43399  rmyeq0  43402  rmyeq  43403  lermy  43404  jm2.27  43457  lsmfgcl  43523  fsumcnsrcl  43615  rngunsnply  43618  gsumws3  44644  mnringmulrcld  44676  nzin  44766  ofdivrec  44774  ofdivcan4  44775  chordthmALT  45380  wessf1ornlem  45636  projf1o  45647  ltdiv23neg  45844  fmulcl  46032  prproropf1olem2  47979  prproropf1olem4  47981  mgmplusgiopALT  48685  itsclc0xyqsolb  49261  toslat  49472  cicerALT  49536