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 2209  ssini 2237  bm1.3ii 2712  elvv 3235  relopab 3273  oprabval5 4036  1st2val 4102  2nd2val 4103  elxp7 4110  df1st2 4133  df2nd2 4134  ster 4275  th3q 4324  fnmap 4336  mapvalg 4337  pmvalg 4338  2dom 4434  endisj 4444  xpmapenlem1 4503  limensuci 4513  phplem2 4516  unfi 4565  unfiOLD 4566  en2lp 4618  aceq6b 4759  zorn 4814  cflecard 4931  cdavalt 4938  uncdadom 4940  cdaen 4943  cda1en 4945  cdaassen 4949  xpcdaen 4950  mulidpq 5088  1lt2pq 5097  1pr 5136  prlem934a 5156  m1p1sr 5220  m1m1sr 5221  0idsr 5225  1idsr 5226  00sr 5227  recexsrlem 5231  addresr 5275  mulresr 5276  ltsor 5280  ax0id 5300  ax1id 5301  axi2m1 5304  axcnre 5305  add4 5361  mul4 5444  muladd 5445  addsub4 5493  renfdisj 5558  recextlem1 5701  muln0 5718  div11t 5773  recrect 5785  divmuldiv 5795  divadddiv 5797  divdivdiv 5798  recdivt 5799  lemulge11t 5857  reclt1t 5907  dfnn2 5945  nnleltp1t 5963  halfpm6th 6041  2halvest 6048  halfaddsubt 6050  nominpos 6052  xrsupsslem 6085  xrinfmsslem 6086  xrsup0 6106  nneo 6206  zneo 6209  dfuz 6211  seqzres 6568  seqzres2 6569  dfseq0 6571  sqr0 6680  sqrlem6 6686  sqrlem8 6688  sqr2gt1lt2 6727  crrecz 6749  nthruc 6753  nthruz 6754  recjt 6825  faclbnd2 6953  faclbnd4lem1 6955  climuni 7106  climaddlem3 7123  climaddc 7139  climmulc 7140  caucvg3a 7171  caucvg3lem 7173  caucvg3t 7175  cvgcmpub 7192  cvgcmp3cetlem1 7195  cvgcmp3cetlem2 7196  infcvglem2 7229  expcnvlem2 7235  expcnvlem5 7238  geolimilem 7242  geolim 7244  geolim1 7246  ivthlem1 7288  ivthlem4 7291  ivthlem8 7295  isupivth 7297  dsupivthlem 7298  efcltlem1 7311  efseq1ex 7313  erelem1 7326  erelem3 7328  ege2le3lem2 7336  ef0 7342  efaddlem6 7350  efaddlem10 7354  efaddlem12 7356  efaddlem20 7364  efaddlem22 7366  efaddlem26 7370  efaddlem27 7371  efaddlem28 7372  ef01tllem2 7391  ef01tllem2OLD 7392  absef01tlub 7395  eirrlem2 7397  eirrlem3 7398  eflegeolem2 7421  eflegeot 7423  efm1legeot 7425  efcnlem4 7429  reeff1olem1 7431  reeff1olem2 7432  efivalt 7454  sinadd 7458  cosadd 7459  cos1bnd 7482  cos2bnd 7483  sincos2sgn 7488  ruclem35 7552  isbasis3g 7619  qdensere 7755  blex 7853  opnm 7864  ioo2bl 7916  tgioo 7919  bcthlem1 8003  bcth 8036  ghgrpi 8140  cnring 8165  ringsn 8166  nvz0 8299  ipid 8366  blocni 8468  ipdirilem 8491  ipasslem6 8498  ipasslem7 8499  siilem1 8514  minveclem16 8563  minveclem19 8566  minveclem25 8572  minveclem27 8574  minveclem38 8585  htthlem12 8634  spwval2 8656  sincolem 8667  pilem1 8673  pilem2 8674  sinhalfpilem 8681  sinperlem1 8688  sincos4thpi 8712  sincos6thpi 8713  efifolem1 8724  efifolem5 8728  efifolem7 8730  efif1lem7 8738  hvadd4 8927  normlem7tALT 8987  hlim0 9107  hlimuni 9111  helch 9118  hsn0elch 9122  hhshsslem2 9140  hhsssh 9141  projlem7 9194  omls 9248  shscl 9283  shintcl 9295  shintclt 9296  chintcl 9297  chintclt 9298  shincl 9333  shsumval2 9362  chincl 9385  chabs1t 9441  fh1 9566  fh2 9567  pjnorm 9668  mayete3 9675  dfiop2 9681  nmopsetn0 9794  nmfnsetn0 9807  lnop0t 9892  lnophmt 9946  nmcopexlem2 9954  nmbdfnlbt 9981  nmcfnexlem2 9983  nlelsh 9995  nmoptri 10029  bdophs 10031  bdopco 10033  nmopcoadj 10036  hmopidmch 10081  hmopidmcht 10083  hmopidmpjt 10084  hstle1t 10156  hst0t 10163  sto1 10166  stle 10170  stji1 10172  strlem3a 10182  strlem5 10185  jplem1 10198  csmdsym 10264  irredt 10325  mdcompl 10359  dmdcompl 10360  cayleylem3 10414  cdrci 10488  hmeogrp 10532  clicls 10601  mslb1 10608  msra3 10610  1ded 10650  relrded 10654  0ded 10669  0cat 10670  1cat 10671  relrcat 10675  isfuna 10733  emhgrat 10754

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