MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3impb Structured version   Visualization version   GIF version

Theorem 3impb 1257
Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.)
Hypothesis
Ref Expression
3impb.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
3impb ((𝜑𝜓𝜒) → 𝜃)

Proof of Theorem 3impb
StepHypRef Expression
1 3impb.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21exp32 630 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1254 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 1038
This theorem is referenced by:  3adant1l  1315  3adant1r  1316  3impdi  1378  rsp2e  3000  vtocl3gf  3259  rspc2ev  3313  reuss  3890  frc  5050  trssord  5709  funtp  5913  resdif  6124  fnotovb  6659  fovrn  6769  fnovrn  6774  fmpt2co  7220  smoord  7422  odi  7619  oeoa  7637  oeoe  7639  nndi  7663  ecopovtrn  7810  ecovass  7815  ecovdi  7816  suppr  8337  infpr  8369  harval2  8783  cdaassen  8964  fin23lem31  9125  tskuni  9565  addasspi  9677  mulasspi  9679  distrpi  9680  mulcanenq  9742  genpass  9791  distrlem1pr  9807  prlem934  9815  ltapr  9827  le2tri3i  10127  subadd  10244  addsub  10252  subdi  10423  submul2  10430  ltaddsub  10462  leaddsub  10464  divval  10647  div12  10667  diveq1  10678  divneg  10679  divdiv2  10697  ltmulgt11  10843  gt0div  10849  ge0div  10850  uzind3  11431  fnn0ind  11436  qdivcl  11769  irrmul  11773  xrlttr  11933  fzen  12316  modcyc  12661  modcyc2  12662  faclbnd4lem4  13039  cshweqdifid  13519  lenegsq  14010  moddvds  14934  dvdscmulr  14953  dvdsmulcr  14954  dvds2add  14958  dvds2sub  14959  dvdsleabs  14976  divalg  15069  divalgb  15070  ndvdsadd  15077  gcdcllem3  15166  dvdslegcd  15169  modgcd  15196  absmulgcd  15209  odzval  15439  pcmul  15499  ressid2  15868  ressval2  15869  catcisolem  16696  prf1st  16784  prf2nd  16785  1st2ndprf  16786  curfuncf  16818  curf2ndf  16827  pltval  16900  pospo  16913  lubel  17062  isdlat  17133  issubmnd  17258  prdsmndd  17263  submcl  17293  grpinvid1  17410  grpinvid2  17411  mulgp1  17514  ghmlin  17605  ghmsub  17608  odlem2  17898  gexlem2  17937  lsmvalx  17994  efgtval  18076  cmncom  18149  lssvnegcl  18896  islss3  18899  prdslmodd  18909  evlslem2  19452  evlseu  19456  zntoslem  19845  maducoeval2  20386  madutpos  20388  madugsum  20389  madurid  20390  m2cpminvid  20498  pm2mpghm  20561  unopn  20648  ntrss  20799  innei  20869  t1sep2  21113  metustsym  22300  cncfi  22637  rrxds  23121  quotval  23985  abelthlem2  24124  mudivsum  25153  padicabv  25253  axsegconlem1  25731  frgrhash2wsp  27089  nsnlplig  27221  nsnlpligALT  27222  grpoinvid1  27270  grpoinvid2  27271  grpodivval  27277  ablo4  27292  ablonncan  27299  nvnpcan  27399  nvmeq0  27401  nvabs  27415  imsdval  27429  ipval  27446  nmorepnf  27511  blo3i  27545  blometi  27546  ipasslem5  27578  hvmulcan  27817  his5  27831  his7  27835  his2sub2  27838  hhssabloilem  28006  hhssnv  28009  fh1  28365  fh2  28366  cm2j  28367  homcl  28493  homco1  28548  homulass  28549  hoadddi  28550  hosubsub2  28559  braadd  28692  bramul  28693  lnopmul  28714  lnopli  28715  lnopaddmuli  28720  lnopsubmuli  28722  lnfnli  28787  lnfnaddmuli  28792  kbass2  28864  mdexchi  29082  xdivval  29454  resvid2  29655  resvval2  29656  unitdivcld  29771  bnj229  30715  bnj546  30727  bnj570  30736  cvmlift2lem7  31052  nosifv  31629  nosires  31630  finminlem  32007  ivthALT  32025  topdifinffinlem  32866  exidcl  33346  grposnOLD  33352  rngoneglmul  33413  rngonegrmul  33414  divrngcl  33427  crngocom  33471  crngm4  33473  inidl  33500  oposlem  33988  hlsuprexch  34186  ldilcnv  34920  ltrnu  34926  tgrpgrplem  35556  tgrpabl  35558  erngdvlem3  35797  erngdvlem3-rN  35805  dvalveclem  35833  dvhfvadd  35899  dvhgrp  35915  dvhlveclem  35916  djhval2  36207  diophren  36896  monotoddzzfi  37026  rpexpmord  37032  ltrmynn0  37034  ltrmxnn0  37035  lermxnn0  37036  rmyeq  37040  lermy  37041  jm2.21  37080  radcnvrat  38034  dvconstbi  38054  expgrowth  38055  bi3impb  38210  eel132  38448  fnotaovb  40612  ccatpfx  40738  submgmcl  41112  onetansqsecsq  41825
  Copyright terms: Public domain W3C validator