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

Theorem 3pm3.2i 1174
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 455 . 2  |-  ( ph  /\ 
ps )
4 3pm3.2i.3 . 2  |-  ch
5 df-3an 975 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
63, 4, 5mpbir2an 920 1  |-  ( ph  /\ 
ps  /\  ch )
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    /\ w3a 973
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 185  df-an 371  df-3an 975
This theorem is referenced by:  mpbir3an  1178  3jaoi  1291  ftp  6083  hartogslem1  7985  cantnflem3  8127  cantnflem4  8128  cantnflem3OLD  8149  cantnflem4OLD  8150  trcl  8176  ttukeylem7  8912  f13idfv  12109  faclbnd4lem1  12374  hashmap  12497  hashge3el3dif  12528  infcvgaux1i  13680  strleun  14742  strle1  14743  slotsbhcdif  14837  estrres  15535  srgbinomlem4  17321  psrass1  18187  psrass23l  18190  psrass23  18192  mplsubrg  18229  mplmon  18252  mplmonmul  18253  mplcoe1  18254  mplbas2  18261  evlslem2  18307  coe1mul2  18437  ply1coeOLD  18465  xrsnsgrp  18581  zfbas  20523  ust0  20848  utop2nei  20879  plypf1  22735  sincos6thpi  23034  1cubr  23299  birthdaylem1  23407  divsqrtsumlem  23435  lgslem2  23698  lgsdir2lem2  23725  lgsdir2lem3  23726  axlowdimlem6  24377  usgraexmpldifpr  24527  2trllemH  24681  2trllemD  24686  2trllemG  24687  wlkntrl  24691  constr2spthlem1  24723  usgra2wlkspthlem2  24747  constr3lem2  24773  constr3trllem2  24778  ex-dvds  25296  sspid  25765  lnocoi  25799  nmlno0lem  25835  nmblolbii  25841  blocnilem  25846  phpar  25866  ip0i  25867  ip2i  25870  ipdirilem  25871  ipasslem10  25881  ip2dii  25886  siilem1  25893  siilem2  25894  hhsst  26309  hhsssh2  26313  fh1i  26666  fh2i  26667  cm2ji  26670  pjoi0i  26763  elunop2  27059  mdslle1i  27363  mdslle2i  27364  mdslj1i  27365  mdslj2i  27366  mdslmd1lem1  27371  mdslmd2i  27376  xrge0iifmhm  28082  cnzh  28112  rezh  28113  dmvlsiga  28302  eulerpartgbij  28508  4bc2eq6  29309  asindmre  30286  areacirc  30296  rabren3dioph  30932  lhe4.4ex1a  31417  fprodge0  31779  fprodge1  31780  stoweidlem13  31977  stoweidlem26  31990  stoweidlem34  31998  stoweid  32027  wallispilem2  32030  fourierdlem62  32133  fourierdlem103  32174  fouriersw  32196  usgra2pthspth  32592  usgra2pthlem1  32594  zlmodzxzldeplem3  33226  zlmodzxzldep  33228  ishlatiN  35202  taupi  37820  inductionexd  38089
  Copyright terms: Public domain W3C validator