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 1332
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 471 . 2 (𝜑𝜓)
4 3pm3.2i.3 . 2 𝜒
5 df-3an 1082 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
63, 4, 5mpbir2an 707 1 (𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 396  w3a 1080
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 1082
This theorem is referenced by:  mpbir3an  1334  3jaoi  1420  ftp  6785  hartogslem1  8855  cantnflem3  9003  cantnflem4  9004  trcl  9019  ttukeylem7  9786  f13idfv  13218  faclbnd4lem1  13503  4bc2eq6  13539  hashge3el3dif  13690  funcnvs3  14112  wrdl3s3  14160  infcvgaux1i  15045  halfleoddlt  15544  strleun  16420  strle1  16421  slotsbhcdif  16522  estrres  17218  srgbinomlem4  18983  psrass1  19873  psrass23l  19876  psrass23  19878  mplsubrg  19908  mplmon  19931  mplmonmul  19932  mplcoe1  19933  mplbas2  19938  evlslem2  19979  coe1mul2  20120  cnfldfun  20239  xrsnsgrp  20263  zfbas  22188  ust0  22511  utop2nei  22542  isclmi0  23385  iscvsi  23416  plypf1  24485  1cubr  25101  birthdaylem1  25211  divsqrtsumlem  25239  lgslem2  25556  lgsdir2lem2  25584  lgsdir2lem3  25585  addsqn2reu  25699  addsqrexnreu  25700  addsqnreup  25701  axlowdimlem6  26416  usgrexmpldifpr  26723  0grsubgr  26743  upgrewlkle2  27071  usgr2wlkspthlem2  27221  usgr2pthlem  27226  elwspths2spth  27428  wlk2v2e  27618  ntrl2v2e  27619  konigsberglem4  27716  konigsberglem5  27717  ex-dvds  27919  sspid  28185  lnocoi  28217  nmlno0lem  28253  nmblolbii  28259  blocnilem  28264  phpar  28284  ip0i  28285  ip2i  28288  ipdirilem  28289  ipasslem10  28299  ip2dii  28304  siilem1  28311  siilem2  28312  hhssabloilem  28721  hhsst  28726  hhsssh2  28730  fh1i  29081  fh2i  29082  cm2ji  29085  pjoi0i  29178  elunop2  29473  mdslle1i  29777  mdslle2i  29778  mdslj1i  29779  mdslj2i  29780  mdslmd1lem1  29785  mdslmd2i  29790  dp2lt  30237  dpadd3  30264  threehalves  30267  cyc3evpm  30422  xrge0slmod  30563  xrge0iifmhm  30791  cnzh  30820  rezh  30821  dmvlsiga  30997  eulerpartgbij  31239  hgt750lemd  31528  hgt750lem  31531  hgt750lemb  31536  hgt750leme  31538  nolt02o  32802  dnizeq0  33417  cnndvlem1  33479  taupi  34148  poimirlem28  34464  poimirlem31  34467  poimirlem32  34468  asindmre  34521  areacirc  34531  ishlatiN  36035  rabren3dioph  38910  inductionexd  40003  lhe4.4ex1a  40212  stoweidlem13  41854  stoweidlem26  41867  stoweidlem34  41875  stoweid  41904  wallispilem2  41907  fourierdlem62  42009  fourierdlem103  42050  fouriersw  42072  salexct3  42181  salgensscntex  42183  smfmullem4  42625  pldofph  42736  31prm  43256  9fppr8  43398  6gbe  43432  8gbe  43434  9gbo  43435  11gbo  43436  nnsum4primesodd  43457  nnsum4primesoddALTV  43458  nnsum4primeseven  43461  tgblthelfgott  43476  tgoldbach  43478  zlmodzxzldeplem3  44051  zlmodzxzldep  44053  blennnt2  44144  line2  44234  line2x  44236  line2y  44237
  Copyright terms: Public domain W3C validator