Theorem pm3.2i 307

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 305	. 2 |- (ph -> (ps -> (ph /\ ps)))
4	1, 2, 3	mp2 54	1 |- (ph /\ ps)

Syntax hints:   /\ wa 240

This theorem is referenced by:  pm4.87 383  dfbi 573  pm3.2ni 640  3pm3.2i 1048  euequ1 1861  unssi 2781  ssini 2816  bm1.3ii 3441  elvv 4053  relopab 4104  funpr 4467  fprOLD 4811  oprabval5 4958  1st2val 5038  2nd2val 5039  elxp7 5042  fparlem3 5083  fparlem4 5084  oeoa 5272  oeoe 5274  ster 5325  th3q 5376  fnmap 5388  mapvalg 5389  pmvalg 5390  endisj 5496  ac6sfi 5509  xpmapenlem1 5590  phplem2 5603  abfii4 5654  en2lp 5707  omsublim 5887  aceq6b 5904  zorn 5959  cflecard 6060  cdaval 6067  uncdadom 6069  cda1en 6076  cdaassen 6080  xpcdaen 6081  nnaun 6089  1lt2pq 6230  1pr 6269  m1p1sr 6353  m1m1sr 6354  recexsrlem 6364  ltsor 6413  axi2m1 6438  axcnre 6439  add4i 6496  mul4i 6588  muladdi 6589  addsub4i 6641  renfdisjOLD 6713  recextlem1 6874  mulne0i 6888  div11 6941  recrec 6952  divmuldivi 6963  divdivdivi 6966  recdiv 6967  divdiv1 6972  divdiv2 6973  lemulge11 7030  dfnn2 7119  halfpm6th 7218  2halves 7225  halfaddsub 7227  xrsupsslem 7285  xrinfmsslem 7286  xrsup0 7306  nneoi 7409  zeo 7411  zneo 7412  dfuzi 7414  cardfz 7719  dfseq0 7806  sqr0 7922  sqrlem6 7928  sqrlem8 7930  sqr2gt1lt2 7969  nthruc 7995  nthruz 7996  recj 8068  faclbnd2 8198  faclbnd4lem1 8200  climuni 8359  climaddci 8392  climmulci 8393  caucvg3ai 8424  caucvg3 8428  cvgcmpubi 8446  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  infcvglem2 8483  expcnvlem2 8489  expcnvlem5 8492  geolimilem 8497  geolim 8499  geolim1i 8500  geolim1 8501  ivthlem1 8543  ivthlem4 8546  ivthlem8 8550  isupivthi 8552  dsupivthlem 8553  efcltlem1 8566  efseq1ex 8568  erelem1 8581  ege2le3lem2 8591  ef0 8597  efaddlem6 8605  efaddlem10 8609  efaddlem12 8611  efaddlem20 8619  efaddlem22 8621  efaddlem23 8622  efaddlem26 8625  efaddlem27 8626  efaddlem28 8627  ef01tllem1 8645  ef01tllem2 8646  ef01tllem2OLD 8647  absef01tlubi 8650  eirrlem2 8652  eirrlem3 8653  egt2lt3 8659  eflegeolem2 8679  eflegeo 8681  efm1legeoi 8682  efm1legeo 8683  efcnlem4 8687  reeff1olem1 8689  reeff1olem2 8690  efi4p 8700  efival 8712  sinaddi 8716  cosaddi 8717  sin01bndlem3 8735  cos01bndlem3 8737  cos1bnd 8740  cos2bnd 8741  cos01gt0 8743  sincos2sgn 8746  ruclem35 8813  isbasis3g 8882  ioo2bl 9190  tgioo 9193  bcth 9310  ghgrpi 9445  cnring 9489  ringsn 9490  nvz0 9628  ipid 9702  blocni 9805  ipdirilem 9829  ipasslem6 9836  ipasslem7 9837  siilem1 9852  minveclem16 9905  minveclem19 9908  minveclem25 9914  minveclem38 9927  htthlem12 9978  spwval2 9996  sincolem 10014  pilem1 10020  pilem2 10021  sinhalfpilem 10028  sincosq4sgn 10056  sinq12gt0t 10057  sincos4thpi 10060  sincos6thpi 10061  coskpi 10064  sineq0 10065  sineq0OLD 10066  efifolem1 10076  efif1lem7 10090  cdrci 10182  clicls 10183  clint3 10184  hvadd4i 10557  normlem7tALT 10618  hlim0 10738  hlimunii 10742  helch 10749  hsn0elch 10753  hhshsslem2 10771  hhsssh 10772  projlem7 10825  omlsi 10879  shscli 10914  shintcli 10926  shintcl 10927  chintcli 10928  chintcl 10929  shincli 10964  shsumval2i 10993  chincli 11016  chabs1 11072  fh1i 11197  fh2i 11198  cm2ji 11201  pjnormi 11301  nmopsetn0 11429  nmfnsetn0 11442  lnophm 11581  nmcopexlem2 11589  nmbdfnlb 11616  nmcfnexlem2 11618  nlelshi 11630  bdophsi 11666  bdopcoi 11668  hmopidmchi 11723  hmopidmch 11725  hmopidmpj 11726  sto1i 11808  stlei 11812  stji1i 11814  csmdsymi 11906  irred 11967  mdcompli 12001  dmdcompli 12002  cayleylem3 13643  divalglem5 13700  divalglem7 13702  gcdaddmlem 13734  mulgcdlem2 13757  1nprm 13769  dfon2lem3 13851  wfii 13916  frindi 13940  poseq 13954  wfrlem13 13969  wfr3 13975  imfstnrelc 14396  repfuntw 14502  domrancur1b 14548  toplat 14638  hmeogrp 14892  prtoptop 14919  clindistop 14962  extopgrp 14980  cntrsetlem 14999  mslb1 15007  msra3 15009  1ded 15085  relrded 15089  0ded 15104  0cat 15105  1cat 15106  relrcat 15110  dualalg 15131  isfuna 15182  catsbc 15197  tarax3d4 15227  omsublimOLD 15396  fneref 15493  refref 15494  filssufil 15571  ufileu 15573  fcluscf 15612  flimfnfcls 15615  filnetlem1 15640  mp4an 15651  prfunOLD 15677  eroprv 15734  fsumltisumi 15823  iihalf1 15872  iihalf2 15873  piececn 15894  cnresoprab 15915  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  heiborlem18 15972  heiborlem32 15986  heiborlem42 15996  bfplem4 16001  bfplem7 16004  bfplem11 16008  bfp 16009  reheibor 16025  phtpycom 16050  phtpycolem1 16051  phtpycolem2 16052  phtpycolem3 16053  phtpycolem4 16054  phtpycolem5 16055  phtpcdm 16061  reparphtlem2 16064  pcoval1 16074  pcoval2 16075  pcocn 16076  pcohtpylem1 16080  pcohtpylem2 16081  pcohtpylem3 16082  pcopt 16084  pcoass 16085  pcorevlem 16086  pi1f 16093  pi1val 16094  emhgrat 16297  pm11.07 16321  ishlati 17019  0psub 17230  atpsub 17233

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 164  df-an 242

Copyright terms: Public domain