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 515  pm3.2ni 580  3pm3.2i 818  unssi 2205  ssini 2233  bm1.3ii 2706  elvv 3228  relopab 3266  oprabval5 4029  1st2val 4095  2nd2val 4096  elxp7 4103  df1st2 4126  df2nd2 4127  ster 4268  th3q 4317  fnmap 4329  mapvalg 4330  pmvalg 4331  2dom 4427  endisj 4437  xpmapenlem1 4496  limensuci 4506  phplem2 4509  unfi 4551  unfiOLD 4552  abfii4OLD 4564  en2lp 4602  aceq6b 4742  zorn 4797  cflecard 4912  cdavalt 4919  uncdadom 4921  cdaen 4924  cda1en 4926  cdaassen 4930  xpcdaen 4931  mulidpq 5069  1lt2pq 5078  1pr 5117  prlem934a 5137  m1p1sr 5201  m1m1sr 5202  0idsr 5206  1idsr 5207  00sr 5208  recexsrlem 5212  addresr 5256  mulresr 5257  ltsor 5261  ax0id 5281  ax1id 5282  axi2m1 5285  axcnre 5286  add4 5342  mul4 5425  muladd 5426  addsub4 5474  renfdisj 5539  recextlem1 5682  muln0 5699  div11t 5765  recrect 5776  divmuldiv 5786  divadddiv 5788  divdivdiv 5789  recdivt 5790  lemulge11t 5848  reclt1t 5898  dfnn2 5936  nnleltp1t 5954  halfpm6th 6032  2halvest 6039  halfaddsubt 6041  nominpos 6043  xrsupsslem 6076  xrinfmsslem 6077  xrsup0 6097  nneo 6197  zneo 6200  dfuz 6202  seqzres 6560  seqzres2 6561  dfseq0 6563  sqr0 6672  sqrlem6 6678  sqrlem8 6680  sqr2gt1lt2 6719  crrecz 6741  nthruc 6745  nthruz 6746  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 7474  cos2bnd 7475  sincos2sgn 7480  ruclem35 7544  isbasis3g 7613  qdensere 7751  blex 7849  opnm 7860  ioo2bl 7912  tgioo 7915  bcthlem1 7999  bcth 8032  ghgrpi 8137  cnring 8162  ringsn 8163  nvz0 8296  ipid 8363  blocni 8465  ipdirilem 8488  ipasslem6 8495  ipasslem7 8496  siilem1 8511  minveclem16 8560  minveclem19 8563  minveclem25 8569  minveclem27 8571  minveclem38 8582  htthlem12 8631  spwval2 8653  sincolem 8665  pilem1 8671  pilem2 8672  sinhalfpilem 8679  sinperlem1 8686  sincos4thpi 8710  sincos6thpi 8711  efifolem1 8722  efifolem5 8726  efifolem7 8728  efif1lem7 8736  hvadd4 8925  normlem7tALT 8985  hlim0 9105  hlimuni 9109  helch 9116  hsn0elch 9120  hhshsslem2 9138  hhsssh 9139  projlem7 9192  omls 9246  shscl 9281  shintcl 9293  shintclt 9294  chintcl 9295  chintclt 9296  shincl 9331  shsumval2 9360  chincl 9383  chabs1t 9439  fh1 9564  fh2 9565  pjnorm 9666  mayete3 9673  dfiop2 9679  nmopsetn0 9792  nmfnsetn0 9805  lnop0t 9890  lnophmt 9944  nmcopexlem2 9952  nmbdfnlbt 9979  nmcfnexlem2 9981  nlelsh 9993  nmoptri 10027  bdophs 10029  bdopco 10031  nmopcoadj 10034  hmopidmch 10079  hmopidmcht 10081  hmopidmpjt 10082  hstle1t 10153  hst0t 10160  sto1 10163  stle 10167  stji1 10169  strlem3a 10179  strlem5 10182  jplem1 10195  csmdsym 10261  irredt 10322  mdcompl 10356  dmdcompl 10357  cayleylem3 10411  cdrci 10494  hmeogrp 10538  clicls 10622  mslb1 10629  msra3 10631  1ded 10671  relrded 10675  0ded 10690  0cat 10691  1cat 10692  relrcat 10696  isfuna 10754  emhgrat 10775

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