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  559  biijust  646  3pm3.2i  1202  sbequilem  1887  unssi  3398  ssini  3448  bm1.3ii  4236  epelg  4416  pwnex  4575  onsucelsucexmid  4657  elvv  4817  relopabiv  4883  funpr  5413  mpov  6151  caovcom  6220  th3q  6887  endisj  7088  phplem2  7120  ssfiexmidt  7146  addnnnq0  7780  mulnnnq0  7781  nqprxx  7877  addsrpr  8076  mulsrpr  8077  recidpirq  8189  apreim  8894  aptap  8941  mulcanapi  8958  div1  8994  recdivap  9009  divdivap1  9014  divdivap2  9015  divassapi  9059  divdirapi  9060  div23api  9061  div11api  9062  divmuldivapi  9063  divmul13api  9064  divadddivapi  9065  divdivdivapi  9066  lemulge11  9157  negiso  9246  2cnne0  9464  2rene0  9465  1mhlfehlf  9473  halfpm6th  9475  2halves  9484  halfaddsub  9489  avglt1  9494  avglt2  9495  div4p1lem1div2  9509  3halfnz  9693  nneoor  9698  zeo  9701  divlt1lt  10075  divle1le  10076  nnledivrp  10117  fz0to4untppr  10480  2tnp1ge0ge0  10685  frecfzennn  10812  xnn0nnen  10823  fxnn0nninf  10825  expge1  10962  faclbnd2  11129  4bc2eq6  11162  cjreb  11576  sqrt2gt1lt2  11759  amgm2  11828  xrnegiso  11972  ege2le3  12382  efi4p  12428  efival  12443  cosmul  12456  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  sincos2sgn  12477  sin4lt0  12478  egt2lt3  12491  3dvdsdec  12576  3dvds2dec  12577  odd2np1  12584  oddge22np1  12592  ltoddhalfle  12604  halfleoddlt  12605  nno  12617  ndvdsi  12644  flodddiv4  12647  flodddiv4lt  12649  flodddiv4t2lthalf  12650  bitsp1o  12664  3lcm2e6woprm  12808  6lcm4e12  12809  pcrec  13031  ballotfilemonn  13165  ballotfilemth  13225  ennnfonelemj0  13236  structfn  13315  ndxslid  13321  strleun  13401  slotsdifipndx  13472  slotsdifplendx  13507  slotsdifdsndx  13522  slotsdifunifndx  13529  cnfld1  14846  expghmap  14881  isbasis3g  15037  bl2in  15394  dveflem  15717  cosz12  15771  sinhalfpilem  15782  ptolemy  15815  sincosq1lem  15816  sincosq4sgn  15820  sinq12gt0  15821  cosq23lt0  15824  coseq00topi  15826  coseq0negpitopi  15827  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  sincos3rdpi  15834  pigt3  15835  coskpi  15839  cos02pilt1  15842  2logb9irrALT  15965  lgsdir2lem1  16027  1lgs  16042  gausslemma2dlem0c  16050  gausslemma2dlem0d  16051  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem3  16062  lgsquad2lem2  16081  2lgslem1a1  16085  2lgslem1a2  16086  2lgslem1c  16089  2lgslem3  16100  2lgsoddprmlem1  16104  usgrexmpldifpr  16370  uhgrsubgrself  16387  konigsberglem1  16609  ex-an  16617  ex-fl  16619  ex-exp  16621  bdbm1.3ii  16787  subctctexmid  16900  qdiff  16959