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

Theorem 3pm3.2i 1183
Description: Infer conjunction of premises. (Contributed by NM, 10-Feb-1995.)
Hypotheses
Ref Expression
3pm3.2i.1  |-  ph
3pm3.2i.2  |-  ps
3pm3.2i.3  |-  ch
Assertion
Ref Expression
3pm3.2i  |-  ( ph  /\ 
ps  /\  ch )

Proof of Theorem 3pm3.2i
StepHypRef Expression
1 3pm3.2i.1 . . 3  |-  ph
2 3pm3.2i.2 . . 3  |-  ps
31, 2pm3.2i 456 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 984 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 928 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  mpbir3an  1187  3jaoi  1327  ftp  6034  hartogslem1  8010  cantnflem3  8148  cantnflem4  8149  trcl  8164  ttukeylem7  8896  f13idfv  12162  faclbnd4lem1  12428  4bc2eq6  12464  hashmap  12555  hashge3el3dif  12590  infcvgaux1i  13858  fprodge0  13990  fprodge1  13992  strleun  15163  strle1  15164  slotsbhcdif  15261  estrres  15967  srgbinomlem4  17719  psrass1  18572  psrass23l  18575  psrass23  18577  mplsubrg  18607  mplmon  18630  mplmonmul  18631  mplcoe1  18632  mplbas2  18637  evlslem2  18678  coe1mul2  18805  ply1coeOLD  18833  xrsnsgrp  18947  zfbas  20853  ust0  21176  utop2nei  21207  plypf1  23108  logblog  23671  1cubr  23710  birthdaylem1  23819  divsqrtsumlem  23847  lgslem2  24167  lgsdir2lem2  24194  lgsdir2lem3  24195  axlowdimlem6  24919  usgraexmpldifpr  25069  2trllemH  25224  2trllemD  25229  2trllemG  25230  wlkntrl  25234  constr2spthlem1  25266  usgra2wlkspthlem2  25290  constr3lem2  25316  constr3trllem2  25321  ex-dvds  25840  sspid  26306  lnocoi  26340  nmlno0lem  26376  nmblolbii  26382  blocnilem  26387  phpar  26407  ip0i  26408  ip2i  26411  ipdirilem  26412  ipasslem10  26422  ip2dii  26427  siilem1  26434  siilem2  26435  hhsst  26859  hhsssh2  26863  fh1i  27216  fh2i  27217  cm2ji  27220  pjoi0i  27313  elunop2  27608  mdslle1i  27912  mdslle2i  27913  mdslj1i  27914  mdslj2i  27915  mdslmd1lem1  27920  mdslmd2i  27925  xrge0slmod  28559  xrge0iifmhm  28697  cnzh  28726  rezh  28727  dmvlsiga  28903  eulerpartgbij  29157  taupi  31631  poimirlem28  31875  poimirlem31  31878  poimirlem32  31879  asindmre  31934  areacirc  31944  ishlatiN  32833  rabren3dioph  35570  inductionexd  36506  lhe4.4ex1a  36591  stoweidlem13  37756  stoweidlem26  37769  stoweidlem34  37778  stoweid  37808  wallispilem2  37811  fourierdlem62  37915  fourierdlem103  37956  fouriersw  37978  pldofph  38347  6gbe  38685  8gbe  38687  9gboa  38688  11gboa  38689  nnsum4primesodd  38704  nnsum4primesoddALTV  38705  nnsum4primeseven  38708  tgblthelfgott  38721  tgoldbach  38724  funsneqopsn  38829  0grsubgr  39087  usgra2pthspth  39256  usgra2pthlem1  39258  zlmodzxzldeplem3  39888  zlmodzxzldep  39890  blennnt2  39993
  Copyright terms: Public domain W3C validator