Theorem pm3.2i 270

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

Syntax hints:   /\ wa 103

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

This theorem is referenced by:  mp4an  423  pm4.87  546  biijust  630  3pm3.2i  1159  sbequilem  1810  unssi  3251  ssini  3299  bm1.3ii  4049  epelg  4212  pwnex  4370  onsucelsucexmid  4445  elvv  4601  funpr  5175  mpov  5861  caovcom  5928  th3q  6534  endisj  6718  phplem2  6747  addnnnq0  7257  mulnnnq0  7258  nqprxx  7354  addsrpr  7553  mulsrpr  7554  recidpirq  7666  apreim  8365  mulcanapi  8428  div1  8463  recdivap  8478  divdivap1  8483  divdivap2  8484  divassapi  8528  divdirapi  8529  div23api  8530  div11api  8531  divmuldivapi  8532  divmul13api  8533  divadddivapi  8534  divdivdivapi  8535  lemulge11  8624  negiso  8713  2cnne0  8929  2rene0  8930  1mhlfehlf  8938  halfpm6th  8940  2halves  8949  halfaddsub  8954  avglt1  8958  avglt2  8959  div4p1lem1div2  8973  3halfnz  9148  nneoor  9153  zeo  9156  divlt1lt  9511  divle1le  9512  nnledivrp  9553  2tnp1ge0ge0  10074  frecfzennn  10199  fxnn0nninf  10211  expge1  10330  faclbnd2  10488  4bc2eq6  10520  cjreb  10638  sqrt2gt1lt2  10821  amgm2  10890  xrnegiso  11031  ege2le3  11377  efi4p  11424  efival  11439  cosmul  11452  sin01bnd  11464  cos01bnd  11465  cos1bnd  11466  cos2bnd  11467  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  sincos2sgn  11472  sin4lt0  11473  egt2lt3  11486  3dvdsdec  11562  3dvds2dec  11563  odd2np1  11570  oddge22np1  11578  ltoddhalfle  11590  halfleoddlt  11591  nno  11603  ndvdsi  11630  flodddiv4  11631  flodddiv4lt  11633  flodddiv4t2lthalf  11634  3lcm2e6woprm  11767  6lcm4e12  11768  ennnfonelemj0  11914  structfn  11978  ndxslid  11984  strleun  12048  isbasis3g  12213  bl2in  12572  dveflem  12855  cosz12  12861  sinhalfpilem  12872  ptolemy  12905  sincosq1lem  12906  sincosq4sgn  12910  sinq12gt0  12911  cosq23lt0  12914  coseq00topi  12916  coseq0negpitopi  12917  tangtx  12919  sincos4thpi  12921  sincos6thpi  12923  sincos3rdpi  12924  pigt3  12925  coskpi  12929  cos02pilt1  12932  ex-an  12935  ex-fl  12937  ex-exp  12939  bdbm1.3ii  13089  subctctexmid  13196