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 1331
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 1081 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
63, 4, 5mpbir2an 707 1 (𝜑𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  wa 396  w3a 1079
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 1081
This theorem is referenced by:  mpbir3an  1333  3jaoi  1419  ftp  6911  hartogslem1  8994  cantnflem3  9142  cantnflem4  9143  trcl  9158  ttukeylem7  9925  f13idfv  13356  faclbnd4lem1  13641  4bc2eq6  13677  hashge3el3dif  13832  funcnvs3  14264  wrdl3s3  14314  infcvgaux1i  15200  halfleoddlt  15699  strleun  16579  strle1  16580  slotsbhcdif  16681  estrres  17377  srgbinomlem4  19222  psrass1  20113  psrass23l  20116  psrass23  20118  mplsubrg  20148  mplmon  20172  mplmonmul  20173  mplcoe1  20174  mplbas2  20179  evlslem2  20220  coe1mul2  20365  cnfldfun  20485  xrsnsgrp  20509  zfbas  22432  ust0  22755  utop2nei  22786  isclmi0  23629  iscvsi  23660  plypf1  24729  1cubr  25347  birthdaylem1  25456  divsqrtsumlem  25484  lgslem2  25801  lgsdir2lem2  25829  lgsdir2lem3  25830  addsqn2reu  25944  addsqrexnreu  25945  addsqnreup  25946  axlowdimlem6  26660  usgrexmpldifpr  26967  0grsubgr  26987  upgrewlkle2  27315  usgr2wlkspthlem2  27466  usgr2pthlem  27471  elwspths2spth  27673  wlk2v2e  27863  ntrl2v2e  27864  konigsberglem4  27961  konigsberglem5  27962  ex-dvds  28162  sspid  28429  lnocoi  28461  nmlno0lem  28497  nmblolbii  28503  blocnilem  28508  phpar  28528  ip0i  28529  ip2i  28532  ipdirilem  28533  ipasslem10  28543  ip2dii  28548  siilem1  28555  siilem2  28556  hhssabloilem  28965  hhsst  28970  hhsssh2  28974  fh1i  29325  fh2i  29326  cm2ji  29329  pjoi0i  29422  elunop2  29717  mdslle1i  30021  mdslle2i  30022  mdslj1i  30023  mdslj2i  30024  mdslmd1lem1  30029  mdslmd2i  30034  dp2lt  30488  dpadd3  30515  threehalves  30518  cyc3evpm  30719  xrge0slmod  30844  xrge0iifmhm  31081  cnzh  31110  rezh  31111  dmvlsiga  31287  eulerpartgbij  31529  hgt750lemd  31818  hgt750lem  31821  hgt750lemb  31826  hgt750leme  31828  nolt02o  33096  dnizeq0  33711  cnndvlem1  33773  taupi  34486  poimirlem28  34801  poimirlem31  34804  poimirlem32  34805  asindmre  34858  areacirc  34868  ishlatiN  36371  rabren3dioph  39290  inductionexd  40383  lhe4.4ex1a  40538  stoweidlem13  42175  stoweidlem26  42188  stoweidlem34  42196  stoweid  42225  wallispilem2  42228  fourierdlem62  42330  fourierdlem103  42371  fouriersw  42393  salexct3  42502  salgensscntex  42504  smfmullem4  42946  pldofph  43058  31prm  43637  9fppr8  43779  6gbe  43813  8gbe  43815  9gbo  43816  11gbo  43817  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  tgblthelfgott  43857  tgoldbach  43859  zlmodzxzldeplem3  44485  zlmodzxzldep  44487  blennnt2  44577  line2  44667  line2x  44669  line2y  44670
  Copyright terms: Public domain W3C validator