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  dfbi 517  pm3.2ni 582  3pm3.2i 820  unssi 2208  ssini 2236  bm1.3ii 2711  elvv 3234  relopab 3272  oprabval5 4035  1st2val 4101  2nd2val 4102  elxp7 4109  df1st2 4132  df2nd2 4133  ster 4274  th3q 4323  fnmap 4335  mapvalg 4336  pmvalg 4337  2dom 4433  endisj 4443  xpmapenlem1 4502  limensuci 4512  phplem2 4515  unfi 4563  unfiOLD 4564  en2lp 4611  aceq6b 4752  zorn 4807  cflecard 4924  cdavalt 4931  uncdadom 4933  cdaen 4936  cda1en 4938  cdaassen 4942  xpcdaen 4943  mulidpq 5081  1lt2pq 5090  1pr 5129  prlem934a 5149  m1p1sr 5213  m1m1sr 5214  0idsr 5218  1idsr 5219  00sr 5220  recexsrlem 5224  addresr 5268  mulresr 5269  ltsor 5273  ax0id 5293  ax1id 5294  axi2m1 5297  axcnre 5298  add4 5354  mul4 5437  muladd 5438  addsub4 5486  renfdisj 5551  recextlem1 5694  muln0 5711  div11t 5766  recrect 5778  divmuldiv 5788  divadddiv 5790  divdivdiv 5791  recdivt 5792  lemulge11t 5850  reclt1t 5900  dfnn2 5938  nnleltp1t 5956  halfpm6th 6034  2halvest 6041  halfaddsubt 6043  nominpos 6045  xrsupsslem 6078  xrinfmsslem 6079  xrsup0 6099  nneo 6199  zneo 6202  dfuz 6204  seqzres 6561  seqzres2 6562  dfseq0 6564  sqr0 6673  sqrlem6 6679  sqrlem8 6681  sqr2gt1lt2 6720  crrecz 6742  nthruc 6746  nthruz 6747  recjt 6818  faclbnd2 6946  faclbnd4lem1 6948  climuni 7099  climaddlem3 7116  climaddc 7132  climmulc 7133  caucvg3a 7164  caucvg3lem 7166  caucvg3t 7168  cvgcmpub 7185  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  infcvglem2 7222  expcnvlem2 7228  expcnvlem5 7231  geolimilem 7235  geolim 7237  geolim1 7239  ivthlem1 7281  ivthlem4 7284  ivthlem8 7288  isupivth 7290  dsupivthlem 7291  efcltlem1 7304  efseq1ex 7306  erelem1 7319  erelem3 7321  ege2le3lem2 7329  ef0 7335  efaddlem6 7343  efaddlem10 7347  efaddlem12 7349  efaddlem20 7357  efaddlem22 7359  efaddlem26 7363  efaddlem27 7364  efaddlem28 7365  ef01tllem2 7384  ef01tllem2OLD 7385  absef01tlub 7388  eirrlem2 7390  eirrlem3 7391  eflegeolem2 7414  eflegeot 7416  efm1legeot 7418  efcnlem4 7422  reeff1olem1 7424  reeff1olem2 7425  efivalt 7447  sinadd 7451  cosadd 7452  cos1bnd 7475  cos2bnd 7476  sincos2sgn 7481  ruclem35 7545  isbasis3g 7612  qdensere 7748  blex 7846  opnm 7857  ioo2bl 7909  tgioo 7912  bcthlem1 7996  bcth 8029  ghgrpi 8133  cnring 8158  ringsn 8159  nvz0 8292  ipid 8359  blocni 8461  ipdirilem 8484  ipasslem6 8491  ipasslem7 8492  siilem1 8507  minveclem16 8556  minveclem19 8559  minveclem25 8565  minveclem27 8567  minveclem38 8578  htthlem12 8627  spwval2 8649  sincolem 8660  pilem1 8666  pilem2 8667  sinhalfpilem 8674  sinperlem1 8681  sincos4thpi 8705  sincos6thpi 8706  efifolem1 8717  efifolem5 8721  efifolem7 8723  efif1lem7 8731  hvadd4 8920  normlem7tALT 8980  hlim0 9100  hlimuni 9104  helch 9111  hsn0elch 9115  hhshsslem2 9133  hhsssh 9134  projlem7 9187  omls 9241  shscl 9276  shintcl 9288  shintclt 9289  chintcl 9290  chintclt 9291  shincl 9326  shsumval2 9355  chincl 9378  chabs1t 9434  fh1 9559  fh2 9560  pjnorm 9661  mayete3 9668  dfiop2 9674  nmopsetn0 9787  nmfnsetn0 9800  lnop0t 9885  lnophmt 9939  nmcopexlem2 9947  nmbdfnlbt 9974  nmcfnexlem2 9976  nlelsh 9988  nmoptri 10022  bdophs 10024  bdopco 10026  nmopcoadj 10029  hmopidmch 10074  hmopidmcht 10076  hmopidmpjt 10077  hstle1t 10148  hst0t 10155  sto1 10158  stle 10162  stji1 10164  strlem3a 10174  strlem5 10177  jplem1 10190  csmdsym 10256  irredt 10317  mdcompl 10351  dmdcompl 10352  cayleylem3 10406  cdrci 10480  hmeogrp 10524  clicls 10593  mslb1 10600  msra3 10602  1ded 10642  relrded 10646  0ded 10661  0cat 10662  1cat 10663  relrcat 10667  isfuna 10725  emhgrat 10746

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