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  4204  epelg  4380  pwnex  4539  onsucelsucexmid  4621  elvv  4780  relopabiv  4844  funpr  5372  mpov  6093  caovcom  6162  th3q  6785  endisj  6979  phplem2  7010  addnnnq0  7632  mulnnnq0  7633  nqprxx  7729  addsrpr  7928  mulsrpr  7929  recidpirq  8041  apreim  8746  aptap  8793  mulcanapi  8810  div1  8846  recdivap  8861  divdivap1  8866  divdivap2  8867  divassapi  8911  divdirapi  8912  div23api  8913  div11api  8914  divmuldivapi  8915  divmul13api  8916  divadddivapi  8917  divdivdivapi  8918  lemulge11  9009  negiso  9098  2cnne0  9316  2rene0  9317  1mhlfehlf  9325  halfpm6th  9327  2halves  9336  halfaddsub  9341  avglt1  9346  avglt2  9347  div4p1lem1div2  9361  3halfnz  9540  nneoor  9545  zeo  9548  divlt1lt  9916  divle1le  9917  nnledivrp  9958  fz0to4untppr  10316  2tnp1ge0ge0  10516  frecfzennn  10643  xnn0nnen  10654  fxnn0nninf  10656  expge1  10793  faclbnd2  10959  4bc2eq6  10991  cjreb  11372  sqrt2gt1lt2  11555  amgm2  11624  xrnegiso  11768  ege2le3  12177  efi4p  12223  efival  12238  cosmul  12251  sin01bnd  12263  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  sincos2sgn  12272  sin4lt0  12273  egt2lt3  12286  3dvdsdec  12371  3dvds2dec  12372  odd2np1  12379  oddge22np1  12387  ltoddhalfle  12399  halfleoddlt  12400  nno  12412  ndvdsi  12439  flodddiv4  12442  flodddiv4lt  12444  flodddiv4t2lthalf  12445  bitsp1o  12459  3lcm2e6woprm  12603  6lcm4e12  12604  pcrec  12826  ennnfonelemj0  12967  structfn  13046  ndxslid  13052  strleun  13132  slotsdifipndx  13203  slotsdifplendx  13238  slotsdifdsndx  13253  slotsdifunifndx  13260  cnfld1  14530  expghmap  14565  isbasis3g  14714  bl2in  15071  dveflem  15394  cosz12  15448  sinhalfpilem  15459  ptolemy  15492  sincosq1lem  15493  sincosq4sgn  15497  sinq12gt0  15498  cosq23lt0  15501  coseq00topi  15503  coseq0negpitopi  15504  tangtx  15506  sincos4thpi  15508  sincos6thpi  15510  sincos3rdpi  15511  pigt3  15512  coskpi  15516  cos02pilt1  15519  2logb9irrALT  15642  lgsdir2lem1  15701  1lgs  15716  gausslemma2dlem0c  15724  gausslemma2dlem0d  15725  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem3  15736  lgsquad2lem2  15755  2lgslem1a1  15759  2lgslem1a2  15760  2lgslem1c  15763  2lgslem3  15774  2lgsoddprmlem1  15778  ex-an  16045  ex-fl  16047  ex-exp  16049  bdbm1.3ii  16212  subctctexmid  16325