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 1259
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 1056 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
63, 4, 5mpbir2an 975 1 (𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 383  w3a 1054
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 385  df-3an 1056
This theorem is referenced by:  mpbir3an  1263  3jaoi  1431  funsneqopsn  6457  ftp  6464  hartogslem1  8488  cantnflem3  8626  cantnflem4  8627  trcl  8642  ttukeylem7  9375  f13idfv  12840  faclbnd4lem1  13120  4bc2eq6  13156  hashmap  13260  hashge3el3dif  13306  funcnvs3  13705  wrdl3s3  13751  infcvgaux1i  14633  fprodge0  14768  fprodge1  14770  halfleoddlt  15133  strleun  16019  strle1  16020  slotsbhcdif  16127  estrres  16826  srgbinomlem4  18589  psrass1  19453  psrass23l  19456  psrass23  19458  mplsubrg  19488  mplmon  19511  mplmonmul  19512  mplcoe1  19513  mplbas2  19518  evlslem2  19560  coe1mul2  19687  cnfldfun  19806  xrsnsgrp  19830  zfbas  21747  ust0  22070  utop2nei  22101  isclmi0  22944  iscvsi  22975  plypf1  24013  logblog  24575  1cubr  24614  birthdaylem1  24723  divsqrtsumlem  24751  lgslem2  25068  lgsdir2lem2  25096  lgsdir2lem3  25097  axlowdimlem6  25872  usgrexmpldifpr  26195  0grsubgr  26215  upgrewlkle2  26558  usgr2wlkspthlem2  26710  usgr2pthlem  26715  elwspths2spth  26934  wlk2v2e  27135  ntrl2v2e  27136  konigsberglem4  27233  konigsberglem5  27234  ex-dvds  27443  sspid  27708  lnocoi  27740  nmlno0lem  27776  nmblolbii  27782  blocnilem  27787  phpar  27807  ip0i  27808  ip2i  27811  ipdirilem  27812  ipasslem10  27822  ip2dii  27827  siilem1  27834  siilem2  27835  hhssabloilem  28246  hhsst  28251  hhsssh2  28255  fh1i  28608  fh2i  28609  cm2ji  28612  pjoi0i  28705  elunop2  29000  mdslle1i  29304  mdslle2i  29305  mdslj1i  29306  mdslj2i  29307  mdslmd1lem1  29312  mdslmd2i  29317  dp2lt  29720  dpadd3  29748  threehalves  29751  xrge0slmod  29972  xrge0iifmhm  30113  cnzh  30142  rezh  30143  dmvlsiga  30320  eulerpartgbij  30562  hgt750lemd  30854  hgt750lem  30857  hgt750lemb  30862  hgt750leme  30864  nolt02o  31970  dnizeq0  32590  cnndvlem1  32653  taupi  33299  poimirlem28  33567  poimirlem31  33570  poimirlem32  33571  asindmre  33625  areacirc  33635  ishlatiN  34960  rabren3dioph  37696  inductionexd  38770  lhe4.4ex1a  38845  stoweidlem13  40548  stoweidlem26  40561  stoweidlem34  40569  stoweid  40598  wallispilem2  40601  fourierdlem62  40703  fourierdlem103  40744  fouriersw  40766  salexct3  40878  salgensscntex  40880  smfmullem4  41322  pldofph  41433  31prm  41837  6gbe  41984  8gbe  41986  9gbo  41987  11gbo  41988  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  tgblthelfgott  42028  tgoldbach  42030  tgblthelfgottOLD  42034  tgoldbachOLD  42037  zlmodzxzldeplem3  42616  zlmodzxzldep  42618  blennnt2  42708
  Copyright terms: Public domain W3C validator