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

Theorem 3pm3.2i 1232
Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
Hypotheses
Ref Expression
3pm3.2i.1 𝜑
3pm3.2i.2 𝜓
3pm3.2i.3 𝜒
Assertion
Ref Expression
3pm3.2i (𝜑𝜓𝜒)

Proof of Theorem 3pm3.2i
StepHypRef Expression
1 3pm3.2i.1 . . 3 𝜑
2 3pm3.2i.2 . . 3 𝜓
31, 2pm3.2i 470 . 2 (𝜑𝜓)
4 3pm3.2i.3 . 2 𝜒
5 df-3an 1033 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
63, 4, 5mpbir2an 957 1 (𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 383  w3a 1031
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 196  df-an 385  df-3an 1033
This theorem is referenced by:  mpbir3an  1237  3jaoi  1383  funsneqopsn  6322  ftp  6329  hartogslem1  8330  cantnflem3  8471  cantnflem4  8472  trcl  8487  ttukeylem7  9220  f13idfv  12662  faclbnd4lem1  12942  4bc2eq6  12978  hashmap  13082  hashge3el3dif  13122  funcnvs3  13509  wrdl3s3  13553  infcvgaux1i  14428  fprodge0  14563  fprodge1  14565  halfleoddlt  14924  strleun  15799  strle1  15800  slotsbhcdif  15903  estrres  16602  srgbinomlem4  18366  psrass1  19226  psrass23l  19229  psrass23  19231  mplsubrg  19261  mplmon  19284  mplmonmul  19285  mplcoe1  19286  mplbas2  19291  evlslem2  19333  coe1mul2  19460  xrsnsgrp  19601  zfbas  21510  ust0  21833  utop2nei  21864  isclmi0  22706  iscvsi  22737  plypf1  23772  logblog  24330  1cubr  24369  birthdaylem1  24478  divsqrtsumlem  24506  lgslem2  24823  lgsdir2lem2  24851  lgsdir2lem3  24852  axlowdimlem6  25627  usgraexmpldifpr  25928  2trllemH  26082  2trllemD  26087  2trllemG  26088  wlkntrl  26092  constr2spthlem1  26124  usgra2wlkspthlem2  26148  constr3lem2  26174  constr3trllem2  26179  ex-dvds  26705  sspid  26964  lnocoi  26996  nmlno0lem  27032  nmblolbii  27038  blocnilem  27043  phpar  27063  ip0i  27064  ip2i  27067  ipdirilem  27068  ipasslem10  27078  ip2dii  27083  siilem1  27090  siilem2  27091  hhssabloilem  27502  hhsst  27507  hhsssh2  27511  fh1i  27864  fh2i  27865  cm2ji  27868  pjoi0i  27961  elunop2  28256  mdslle1i  28560  mdslle2i  28561  mdslj1i  28562  mdslj2i  28563  mdslmd1lem1  28568  mdslmd2i  28573  xrge0slmod  29175  xrge0iifmhm  29313  cnzh  29342  rezh  29343  dmvlsiga  29519  eulerpartgbij  29761  dnizeq0  31635  cnndvlem1  31698  taupi  32346  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  asindmre  32665  areacirc  32675  ishlatiN  33660  rabren3dioph  36397  inductionexd  37473  lhe4.4ex1a  37550  stoweidlem13  38906  stoweidlem26  38919  stoweidlem34  38927  stoweid  38956  wallispilem2  38959  fourierdlem62  39061  fourierdlem103  39102  fouriersw  39124  salexct3  39236  salgensscntex  39238  smfmullem4  39679  pldofph  39761  31prm  40050  6gbe  40193  8gbe  40195  9gboa  40196  11gboa  40197  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  nnsum4primeseven  40216  tgblthelfgott  40229  tgoldbach  40232  tgblthelfgottOLD  40236  tgoldbachOLD  40239  0grsubgr  40502  upgrewlkle2  40808  usgr2wlkspthlem2  40964  usgr2pthlem  40969  elwspths2spth  41171  1wlk2v2e  41324  ntrl2v2e  41325  konigsberglem4  41425  konigsberglem5  41426  zlmodzxzldeplem3  42085  zlmodzxzldep  42087  blennnt2  42181
  Copyright terms: Public domain W3C validator