Theorem pm3.2i 272

Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)

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

Syntax hints:   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mp4an  427  pm4.87  557  biijust  642  3pm3.2i  1177  sbequilem  1852  unssi  3338  ssini  3386  bm1.3ii  4154  epelg  4325  pwnex  4484  onsucelsucexmid  4566  elvv  4725  relopabiv  4789  funpr  5310  mpov  6012  caovcom  6081  th3q  6699  endisj  6883  phplem2  6914  addnnnq0  7516  mulnnnq0  7517  nqprxx  7613  addsrpr  7812  mulsrpr  7813  recidpirq  7925  apreim  8630  aptap  8677  mulcanapi  8694  div1  8730  recdivap  8745  divdivap1  8750  divdivap2  8751  divassapi  8795  divdirapi  8796  div23api  8797  div11api  8798  divmuldivapi  8799  divmul13api  8800  divadddivapi  8801  divdivdivapi  8802  lemulge11  8893  negiso  8982  2cnne0  9200  2rene0  9201  1mhlfehlf  9209  halfpm6th  9211  2halves  9220  halfaddsub  9225  avglt1  9230  avglt2  9231  div4p1lem1div2  9245  3halfnz  9423  nneoor  9428  zeo  9431  divlt1lt  9799  divle1le  9800  nnledivrp  9841  fz0to4untppr  10199  2tnp1ge0ge0  10391  frecfzennn  10518  xnn0nnen  10529  fxnn0nninf  10531  expge1  10668  faclbnd2  10834  4bc2eq6  10866  cjreb  11031  sqrt2gt1lt2  11214  amgm2  11283  xrnegiso  11427  ege2le3  11836  efi4p  11882  efival  11897  cosmul  11910  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  sincos2sgn  11931  sin4lt0  11932  egt2lt3  11945  3dvdsdec  12030  3dvds2dec  12031  odd2np1  12038  oddge22np1  12046  ltoddhalfle  12058  halfleoddlt  12059  nno  12071  ndvdsi  12098  flodddiv4  12101  flodddiv4lt  12103  flodddiv4t2lthalf  12104  bitsp1o  12117  3lcm2e6woprm  12254  6lcm4e12  12255  pcrec  12477  ennnfonelemj0  12618  structfn  12697  ndxslid  12703  strleun  12782  slotsdifipndx  12852  slotsdifplendx  12887  slotsdifdsndx  12898  slotsdifunifndx  12905  cnfld1  14128  expghmap  14163  isbasis3g  14282  bl2in  14639  dveflem  14962  cosz12  15016  sinhalfpilem  15027  ptolemy  15060  sincosq1lem  15061  sincosq4sgn  15065  sinq12gt0  15066  cosq23lt0  15069  coseq00topi  15071  coseq0negpitopi  15072  tangtx  15074  sincos4thpi  15076  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  coskpi  15084  cos02pilt1  15087  2logb9irrALT  15210  lgsdir2lem1  15269  1lgs  15284  gausslemma2dlem0c  15292  gausslemma2dlem0d  15293  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem3  15304  lgsquad2lem2  15323  2lgslem1a1  15327  2lgslem1a2  15328  2lgslem1c  15331  2lgslem3  15342  2lgsoddprmlem1  15346  ex-an  15369  ex-fl  15371  ex-exp  15373  bdbm1.3ii  15537  subctctexmid  15645