Theorem pm3.2i 285

Description: Infer conjunction of premises.

Hypotheses

Ref	Expression
pm3.2i.1	|- ph
pm3.2i.2	|- ps

Assertion

Ref	Expression
pm3.2i	|- (ph /\ ps)

Proof of Theorem pm3.2i

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 |- ph
2		pm3.2i.2	. 2 |- ps
3		pm3.2 283	. 2 |- (ph -> (ps -> (ph /\ ps)))
4	1, 2, 3	mp2 43	1 |- (ph /\ ps)

Syntax hints:   /\ wa 223

This theorem is referenced by:  pm4.87 356  pm3.2ni 578  3pm3.2i 816  unssi 2195  ssini 2223  bm1.3ii 2696  elvv 3218  relopab 3256  oprabval5 4014  1st2val 4079  2nd2val 4080  elxp7 4087  df1st2 4110  df2nd2 4111  ster 4252  th3q 4301  fnmap 4313  mapvalg 4314  pmvalg 4315  2dom 4408  endisj 4417  xpmapenlem1 4476  limensuci 4486  phplem2 4489  unfi 4528  abfii4 4538  en2lp 4574  aceq6b 4714  zorn 4769  cflecard 4884  cdavalt 4891  uncdadom 4893  cdaen 4896  cda1en 4898  cdaassen 4902  xpcdaen 4903  mulidpq 5041  1lt2pq 5050  1pr 5089  prlem934a 5109  m1p1sr 5173  m1m1sr 5174  0idsr 5178  1idsr 5179  00sr 5180  recexsrlem 5184  addresr 5228  mulresr 5229  ltsor 5233  ax0id 5253  ax1id 5254  axi2m1 5257  axcnre 5258  add4 5314  mul4 5397  muladd 5398  addsub4 5446  renfdisj 5512  recextlem1 5655  muln0 5668  div11t 5721  recrect 5732  divmuldiv 5742  divadddiv 5744  divdivdiv 5745  recdivt 5746  reclt1t 5846  dfnn2 5884  nnleltp1t 5901  halfpm6th 5979  nominpos 5990  xrsupsslem 6023  xrinfmsslem 6024  xrsup0 6044  dfuz 6150  seqzres 6492  seqzres2 6493  dfseq0 6495  sqr0 6602  sqrlem6 6608  sqrlem8 6610  sqr2gt1lt2 6649  crrecz 6672  nthruc 6676  nthruz 6677  faclbnd2 6883  faclbnd4lem1 6885  climuni 7036  climaddlem3 7052  climaddc 7068  climmulc 7069  caucvg3a 7100  caucvg3lem 7102  caucvg3t 7104  cvgcmpub 7121  cvgcmp3cetlem1 7124  cvgcmp3cetlem2 7125  infcvglem2 7157  expcnvlem2 7163  expcnvlem5 7166  geolimilem 7170  geolim 7172  geolim1 7174  ivthlem1 7216  ivthlem4 7219  ivthlem8 7223  isupivth 7225  dsupivthlem 7226  ivthlem4OLD 7228  ivthlem8OLD 7232  efcltlem1 7246  efseq1ex 7248  erelem1 7261  erelem3 7263  ege2le3lem2 7271  ef0 7277  efaddlem6 7285  efaddlem10 7289  efaddlem12 7291  efaddlem20 7299  efaddlem22 7301  efaddlem26 7305  efaddlem27 7306  efaddlem28 7307  ef01tllem2 7326  absef01tlub 7329  eirrlem2 7331  eirrlem3 7332  eflegeolem2 7354  eflegeot 7356  efm1legeot 7358  efcnlem4 7362  reeff1olem1 7364  reeff1olem2 7365  reeff1olem1OLD 7366  reeff1olem2OLD 7367  sinadd 7393  cosadd 7394  cos1bnd 7416  cos2bnd 7417  sincos2sgn 7422  ruclem35 7487  isbasis3g 7555  qdensere 7691  blex 7789  opnm 7800  tgioo 7854  bcthlem1 7933  bcth 7966  ghgrpi 8074  cnring 8099  ringsn 8100  nvz0 8235  ipid 8297  blocni 8396  ipdirilem 8419  ipasslem6 8426  ipasslem7 8427  siilem1 8442  minveclem16 8491  minveclem19 8494  minveclem25 8500  minveclem27 8502  minveclem38 8513  htthlem12 8561  spwval2 8577  sincolem 8584  pilem1 8590  pilem2 8591  sinhalfpilem 8598  sinperlem1 8605  sincos4thpi 8627  sincos6thpi 8628  efifolem1 8637  efifolem5 8641  efifolem7 8643  efif1lem7 8651  hvadd4 8846  normlem7tALT 8906  hlim0 9026  hlimuni 9030  helch 9037  hsn0elch 9041  hhshsslem2 9058  hhsssh 9059  projlem7 9108  omls 9161  shscl 9196  shintcl 9208  shintclt 9209  chintcl 9210  chintclt 9211  shincl 9246  shsumval2 9275  chincl 9298  chabs1t 9354  fh1 9481  fh2 9482  pjnorm 9583  mayete3 9590  dfiop2 9596  nmopsetn0 9709  nmfnsetn0 9722  lnop0t 9806  lnophmt 9859  nmcopexlem2 9867  nmbdfnlbt 9894  nmcfnexlem2 9896  nlelsh 9908  nmoptri 9941  bdophs 9943  bdopco 9945  nmopcoadj 9948  hmopidmch 9990  hmopidmcht 9992  hmopidmpjt 9993  hstle1t 10063  hst0t 10070  sto1 10073  stle 10077  stji1 10079  strlem3a 10089  strlem5 10092  jplem1 10105  csmdsym 10169  irredt 10230  mdcompl 10261  dmdcompl 10262  cayleylem3 10318  cdrci 10381  hmeogrp 10425  clicls 10466  1ded 10515  relrded 10519  0ded 10534  0cat 10535  1cat 10536  relrcat 10540  isfuna 10592  emhgrat 10611

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain