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

Theorem 3impb 1251
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 628 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1248 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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 195  df-an 384  df-3an 1032
This theorem is referenced by:  3adant1l  1309  3adant1r  1310  3impdi  1372  rsp2e  2986  vtocl3gf  3241  rspc2ev  3294  reuss  3866  frc  4994  trssord  5643  funtp  5845  resdif  6055  fnotovb  6570  fovrn  6679  fnovrn  6684  fmpt2co  7124  smoord  7326  odi  7523  oeoa  7541  oeoe  7543  nndi  7567  ecopovtrn  7714  ecovass  7719  ecovdi  7720  suppr  8237  infpr  8269  harval2  8683  cdaassen  8864  fin23lem31  9025  tskuni  9461  addasspi  9573  mulasspi  9575  distrpi  9576  mulcanenq  9638  genpass  9687  distrlem1pr  9703  prlem934  9711  ltapr  9723  le2tri3i  10018  subadd  10135  addsub  10143  subdi  10314  submul2  10321  ltaddsub  10351  leaddsub  10353  divval  10536  div12  10556  diveq1  10567  divneg  10568  divdiv2  10586  ltmulgt11  10732  gt0div  10738  ge0div  10739  uzind3  11303  fnn0ind  11308  qdivcl  11641  irrmul  11645  xrlttr  11808  fzen  12184  modcyc  12522  modcyc2  12523  faclbnd4lem4  12900  cshweqdifid  13363  lenegsq  13854  moddvds  14775  dvdscmulr  14794  dvdsmulcr  14795  dvds2add  14799  dvds2sub  14800  dvdsleabs  14817  divalg  14910  divalgb  14911  ndvdsadd  14918  gcdcllem3  15007  dvdslegcd  15010  modgcd  15037  absmulgcd  15050  odzval  15280  pcmul  15340  ressid2  15701  ressval2  15702  catcisolem  16525  prf1st  16613  prf2nd  16614  1st2ndprf  16615  curfuncf  16647  curf2ndf  16656  pltval  16729  pospo  16742  lubel  16891  isdlat  16962  issubmnd  17087  prdsmndd  17092  submcl  17122  grpinvid1  17239  grpinvid2  17240  mulgp1  17343  ghmlin  17434  ghmsub  17437  odlem2  17727  gexlem2  17766  lsmvalx  17823  efgtval  17905  cmncom  17978  lssvnegcl  18723  islss3  18726  prdslmodd  18736  evlslem2  19279  evlseu  19283  zntoslem  19669  maducoeval2  20207  madutpos  20209  madugsum  20210  madurid  20211  m2cpminvid  20319  pm2mpghm  20382  unopn  20475  ntrss  20611  innei  20681  t1sep2  20925  metustsym  22111  cncfi  22436  rrxds  22906  quotval  23768  abelthlem2  23907  mudivsum  24936  padicabv  25036  axsegconlem1  25515  frgregordn0  26363  grpoinvid1  26532  grpoinvid2  26533  grpodivval  26539  ablo4  26557  ablonncan  26564  vcnegsubdi2OLD  26596  nvnpcan  26685  nvmeq0  26689  nvabs  26706  imsdval  26722  ipval  26743  nmorepnf  26813  blo3i  26847  blometi  26848  ipasslem5  26880  hvmulcan  27119  his5  27133  his7  27137  his2sub2  27140  hhssabloilem  27308  hhssnv  27311  fh1  27667  fh2  27668  cm2j  27669  homcl  27795  homco1  27850  homulass  27851  hoadddi  27852  hosubsub2  27861  braadd  27994  bramul  27995  lnopmul  28016  lnopli  28017  lnopaddmuli  28022  lnopsubmuli  28024  lnfnli  28089  lnfnaddmuli  28094  kbass2  28166  mdexchi  28384  xdivval  28764  resvid2  28965  resvval2  28966  unitdivcld  29081  bnj229  30014  bnj546  30026  bnj570  30035  cvmlift2lem7  30351  finminlem  31288  ivthALT  31306  topdifinffinlem  32174  exidcl  32648  grposnOLD  32654  rngoneglmul  32715  rngonegrmul  32716  divrngcl  32729  crngocom  32773  crngm4  32775  inidl  32802  oposlem  33290  hlsuprexch  33488  ldilcnv  34222  ltrnu  34228  tgrpgrplem  34858  tgrpabl  34860  erngdvlem3  35099  erngdvlem3-rN  35107  dvalveclem  35135  dvhfvadd  35201  dvhgrp  35217  dvhlveclem  35218  djhval2  35509  diophren  36198  monotoddzzfi  36328  rpexpmord  36334  ltrmynn0  36336  ltrmxnn0  36337  lermxnn0  36338  rmyeq  36342  lermy  36343  jm2.21  36382  radcnvrat  37338  dvconstbi  37358  expgrowth  37359  bi3impb  37513  eel132  37751  fnotaovb  39732  ccatpfx  40077  frgrhash2wsp  41499  submgmcl  41586  onetansqsecsq  42264
  Copyright terms: Public domain W3C validator