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 1424
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 1074 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
63, 4, 5mpbir2an 993 1 (𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 383  w3a 1072
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 1074
This theorem is referenced by:  mpbir3an  1427  3jaoi  1540  funsneqopsn  6580  ftp  6587  hartogslem1  8612  cantnflem3  8761  cantnflem4  8762  trcl  8777  ttukeylem7  9529  f13idfv  12994  faclbnd4lem1  13274  4bc2eq6  13310  hashmap  13414  hashge3el3dif  13460  funcnvs3  13859  wrdl3s3  13906  infcvgaux1i  14788  fprodge0  14923  fprodge1  14925  halfleoddlt  15288  strleun  16174  strle1  16175  slotsbhcdif  16282  estrres  16980  srgbinomlem4  18743  psrass1  19607  psrass23l  19610  psrass23  19612  mplsubrg  19642  mplmon  19665  mplmonmul  19666  mplcoe1  19667  mplbas2  19672  evlslem2  19714  coe1mul2  19841  cnfldfun  19960  xrsnsgrp  19984  zfbas  21901  ust0  22224  utop2nei  22255  isclmi0  23098  iscvsi  23129  plypf1  24167  logblog  24729  1cubr  24768  birthdaylem1  24877  divsqrtsumlem  24905  lgslem2  25222  lgsdir2lem2  25250  lgsdir2lem3  25251  axlowdimlem6  26026  usgrexmpldifpr  26349  0grsubgr  26369  upgrewlkle2  26712  usgr2wlkspthlem2  26864  usgr2pthlem  26869  elwspths2spth  27089  wlk2v2e  27309  ntrl2v2e  27310  konigsberglem4  27407  konigsberglem5  27408  ex-dvds  27624  sspid  27889  lnocoi  27921  nmlno0lem  27957  nmblolbii  27963  blocnilem  27968  phpar  27988  ip0i  27989  ip2i  27992  ipdirilem  27993  ipasslem10  28003  ip2dii  28008  siilem1  28015  siilem2  28016  hhssabloilem  28427  hhsst  28432  hhsssh2  28436  fh1i  28789  fh2i  28790  cm2ji  28793  pjoi0i  28886  elunop2  29181  mdslle1i  29485  mdslle2i  29486  mdslj1i  29487  mdslj2i  29488  mdslmd1lem1  29493  mdslmd2i  29498  dp2lt  29901  dpadd3  29929  threehalves  29932  xrge0slmod  30153  xrge0iifmhm  30294  cnzh  30323  rezh  30324  dmvlsiga  30501  eulerpartgbij  30743  hgt750lemd  31035  hgt750lem  31038  hgt750lemb  31043  hgt750leme  31045  nolt02o  32151  dnizeq0  32771  cnndvlem1  32834  taupi  33480  poimirlem28  33750  poimirlem31  33753  poimirlem32  33754  asindmre  33808  areacirc  33818  ishlatiN  35145  rabren3dioph  37881  inductionexd  38955  lhe4.4ex1a  39030  stoweidlem13  40733  stoweidlem26  40746  stoweidlem34  40754  stoweid  40783  wallispilem2  40786  fourierdlem62  40888  fourierdlem103  40929  fouriersw  40951  salexct3  41063  salgensscntex  41065  smfmullem4  41507  pldofph  41618  31prm  42022  6gbe  42169  8gbe  42171  9gbo  42172  11gbo  42173  nnsum4primesodd  42194  nnsum4primesoddALTV  42195  nnsum4primeseven  42198  tgblthelfgott  42213  tgoldbach  42215  tgblthelfgottOLD  42219  tgoldbachOLD  42222  zlmodzxzldeplem3  42801  zlmodzxzldep  42803  blennnt2  42893
  Copyright terms: Public domain W3C validator