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  644  3pm3.2i  1199  sbequilem  1884  unssi  3379  ssini  3427  bm1.3ii  4205  epelg  4381  pwnex  4540  onsucelsucexmid  4622  elvv  4781  relopabiv  4845  funpr  5373  mpov  6100  caovcom  6169  th3q  6795  endisj  6991  phplem2  7022  addnnnq0  7647  mulnnnq0  7648  nqprxx  7744  addsrpr  7943  mulsrpr  7944  recidpirq  8056  apreim  8761  aptap  8808  mulcanapi  8825  div1  8861  recdivap  8876  divdivap1  8881  divdivap2  8882  divassapi  8926  divdirapi  8927  div23api  8928  div11api  8929  divmuldivapi  8930  divmul13api  8931  divadddivapi  8932  divdivdivapi  8933  lemulge11  9024  negiso  9113  2cnne0  9331  2rene0  9332  1mhlfehlf  9340  halfpm6th  9342  2halves  9351  halfaddsub  9356  avglt1  9361  avglt2  9362  div4p1lem1div2  9376  3halfnz  9555  nneoor  9560  zeo  9563  divlt1lt  9932  divle1le  9933  nnledivrp  9974  fz0to4untppr  10332  2tnp1ge0ge0  10533  frecfzennn  10660  xnn0nnen  10671  fxnn0nninf  10673  expge1  10810  faclbnd2  10976  4bc2eq6  11008  cjreb  11392  sqrt2gt1lt2  11575  amgm2  11644  xrnegiso  11788  ege2le3  12197  efi4p  12243  efival  12258  cosmul  12271  sin01bnd  12283  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  sincos2sgn  12292  sin4lt0  12293  egt2lt3  12306  3dvdsdec  12391  3dvds2dec  12392  odd2np1  12399  oddge22np1  12407  ltoddhalfle  12419  halfleoddlt  12420  nno  12432  ndvdsi  12459  flodddiv4  12462  flodddiv4lt  12464  flodddiv4t2lthalf  12465  bitsp1o  12479  3lcm2e6woprm  12623  6lcm4e12  12624  pcrec  12846  ennnfonelemj0  12987  structfn  13066  ndxslid  13072  strleun  13152  slotsdifipndx  13223  slotsdifplendx  13258  slotsdifdsndx  13273  slotsdifunifndx  13280  cnfld1  14551  expghmap  14586  isbasis3g  14735  bl2in  15092  dveflem  15415  cosz12  15469  sinhalfpilem  15480  ptolemy  15513  sincosq1lem  15514  sincosq4sgn  15518  sinq12gt0  15519  cosq23lt0  15522  coseq00topi  15524  coseq0negpitopi  15525  tangtx  15527  sincos4thpi  15529  sincos6thpi  15531  sincos3rdpi  15532  pigt3  15533  coskpi  15537  cos02pilt1  15540  2logb9irrALT  15663  lgsdir2lem1  15722  1lgs  15737  gausslemma2dlem0c  15745  gausslemma2dlem0d  15746  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem3  15757  lgsquad2lem2  15776  2lgslem1a1  15780  2lgslem1a2  15781  2lgslem1c  15784  2lgslem3  15795  2lgsoddprmlem1  15799  ex-an  16142  ex-fl  16144  ex-exp  16146  bdbm1.3ii  16309  subctctexmid  16425