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

Theorem 3impb 1109
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 421 . 2 (𝜑 → (𝜓 → (𝜒𝜃)))
323imp 1105 1 ((𝜑𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  3adant3  1126  3impdi  1344  rsp2e  3310  vtocl3gf  3576  rspc2ev  3639  reuss  4288  frc  5520  trssord  6207  funtp  6410  resdif  6634  fnotovb  7200  fovrn  7312  fnovrn  7317  fmpoco  7786  smoord  7998  odi  8200  oeoa  8218  oeoe  8220  nndi  8244  ecopovtrn  8395  ecovass  8399  ecovdi  8400  suppr  8929  infpr  8961  harval2  9420  fin23lem31  9759  tskuni  10199  addasspi  10311  mulasspi  10313  distrpi  10314  mulcanenq  10376  genpass  10425  distrlem1pr  10441  prlem934  10449  ltapr  10461  le2tri3i  10764  subadd  10883  addsub  10891  subdi  11067  submul2  11074  ltaddsub  11108  leaddsub  11110  divval  11294  div12  11314  diveq1  11325  divneg  11326  divdiv2  11346  ltmulgt11  11494  gt0div  11500  ge0div  11501  uzind3  12070  fnn0ind  12075  qdivcl  12364  irrmul  12368  xrlttr  12528  fzen  12919  modcyc  13269  modcyc2  13270  rpexpmord  13527  faclbnd4lem4  13651  ccatval21sw  13934  lswccatn0lsw  13940  ccatpfx  14058  ccatopth  14073  cshweqdifid  14177  lenegsq  14675  moddvds  15613  dvdscmulr  15633  dvdsmulcr  15634  dvds2add  15638  dvds2sub  15639  dvdsleabs  15656  divalg  15749  divalgb  15750  ndvdsadd  15756  gcdcllem3  15845  dvdslegcd  15848  modgcd  15875  absmulgcd  15892  odzval  16123  pcmul  16183  ressid2  16547  ressval2  16548  catcisolem  17361  prf1st  17449  prf2nd  17450  1st2ndprf  17451  curfuncf  17483  curf2ndf  17492  pltval  17565  pospo  17578  lubel  17727  isdlat  17798  issubmnd  17933  prdsmndd  17939  submcl  17972  grpinvid1  18099  grpinvid2  18100  mulgp1  18205  ghmlin  18308  ghmsub  18311  odlem2  18603  gexlem2  18643  lsmvalx  18700  efgtval  18785  cmncom  18859  lssvnegcl  19664  islss3  19667  prdslmodd  19677  evlslem2  20227  evlseu  20231  zntoslem  20638  maducoeval2  21184  madutpos  21186  madugsum  21187  madurid  21188  m2cpminvid  21296  pm2mpghm  21359  unopn  21446  ntrss  21598  innei  21668  t1sep2  21912  metustsym  23099  cncfi  23436  rrxds  23930  quotval  24815  abelthlem2  24954  mudivsum  26039  padicabv  26139  axsegconlem1  26636  nsnlplig  28191  nsnlpligALT  28192  grpoinvid1  28238  grpoinvid2  28239  grpodivval  28245  ablo4  28260  ablonncan  28266  nvnpcan  28366  nvmeq0  28368  nvabs  28382  imsdval  28396  ipval  28413  nmorepnf  28478  blo3i  28512  blometi  28513  ipasslem5  28545  hvmulcan  28782  his5  28796  his7  28800  his2sub2  28803  hhssabloilem  28971  hhssnv  28974  fh1  29328  fh2  29329  cm2j  29330  homcl  29456  homco1  29511  homulass  29512  hoadddi  29513  hosubsub2  29522  braadd  29655  bramul  29656  lnopmul  29677  lnopli  29678  lnopaddmuli  29683  lnopsubmuli  29685  lnfnli  29750  lnfnaddmuli  29755  kbass2  29827  mdexchi  30045  xdivval  30528  resvid2  30834  resvval2  30835  fedgmullem2  30931  unitdivcld  31049  bnj229  32061  bnj546  32073  bnj570  32082  cusgredgex2  32272  loop1cycl  32287  cvmlift2lem7  32459  nosupfv  33109  nosupres  33110  finminlem  33569  ivthALT  33586  topdifinffinlem  34516  lindsadd  34771  exidcl  35041  grposnOLD  35047  rngoneglmul  35108  rngonegrmul  35109  divrngcl  35122  crngocom  35166  crngm4  35168  inidl  35195  xrninxpex  35528  oposlem  36204  hlsuprexch  36403  ldilcnv  37137  ltrnu  37143  tgrpgrplem  37771  tgrpabl  37773  erngdvlem3  38012  erngdvlem3-rN  38020  dvalveclem  38047  dvhfvadd  38113  dvhgrp  38129  dvhlveclem  38130  djhval2  38421  resubadd  39093  diophren  39294  monotoddzzfi  39423  ltrmynn0  39429  ltrmxnn0  39430  lermxnn0  39431  rmyeq  39435  lermy  39436  jm2.21  39475  radcnvrat  40530  dvconstbi  40550  expgrowth  40551  bi3impb  40701  eel132  40920  xlimmnfvlem2  41998  xlimpnfvlem2  42002  fnotaovb  43282  submgmcl  43912  onetansqsecsq  44762
  Copyright terms: Public domain W3C validator