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  3380  ssini  3428  bm1.3ii  4208  epelg  4385  pwnex  4544  onsucelsucexmid  4626  elvv  4786  relopabiv  4851  funpr  5379  mpov  6106  caovcom  6175  th3q  6804  endisj  7003  phplem2  7034  addnnnq0  7659  mulnnnq0  7660  nqprxx  7756  addsrpr  7955  mulsrpr  7956  recidpirq  8068  apreim  8773  aptap  8820  mulcanapi  8837  div1  8873  recdivap  8888  divdivap1  8893  divdivap2  8894  divassapi  8938  divdirapi  8939  div23api  8940  div11api  8941  divmuldivapi  8942  divmul13api  8943  divadddivapi  8944  divdivdivapi  8945  lemulge11  9036  negiso  9125  2cnne0  9343  2rene0  9344  1mhlfehlf  9352  halfpm6th  9354  2halves  9363  halfaddsub  9368  avglt1  9373  avglt2  9374  div4p1lem1div2  9388  3halfnz  9567  nneoor  9572  zeo  9575  divlt1lt  9949  divle1le  9950  nnledivrp  9991  fz0to4untppr  10349  2tnp1ge0ge0  10551  frecfzennn  10678  xnn0nnen  10689  fxnn0nninf  10691  expge1  10828  faclbnd2  10994  4bc2eq6  11026  cjreb  11417  sqrt2gt1lt2  11600  amgm2  11669  xrnegiso  11813  ege2le3  12222  efi4p  12268  efival  12283  cosmul  12296  sin01bnd  12308  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  sincos2sgn  12317  sin4lt0  12318  egt2lt3  12331  3dvdsdec  12416  3dvds2dec  12417  odd2np1  12424  oddge22np1  12432  ltoddhalfle  12444  halfleoddlt  12445  nno  12457  ndvdsi  12484  flodddiv4  12487  flodddiv4lt  12489  flodddiv4t2lthalf  12490  bitsp1o  12504  3lcm2e6woprm  12648  6lcm4e12  12649  pcrec  12871  ennnfonelemj0  13012  structfn  13091  ndxslid  13097  strleun  13177  slotsdifipndx  13248  slotsdifplendx  13283  slotsdifdsndx  13298  slotsdifunifndx  13305  cnfld1  14576  expghmap  14611  isbasis3g  14760  bl2in  15117  dveflem  15440  cosz12  15494  sinhalfpilem  15505  ptolemy  15538  sincosq1lem  15539  sincosq4sgn  15543  sinq12gt0  15544  cosq23lt0  15547  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  sincos6thpi  15556  sincos3rdpi  15557  pigt3  15558  coskpi  15562  cos02pilt1  15565  2logb9irrALT  15688  lgsdir2lem1  15747  1lgs  15762  gausslemma2dlem0c  15770  gausslemma2dlem0d  15771  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquad2lem2  15801  2lgslem1a1  15805  2lgslem1a2  15806  2lgslem1c  15809  2lgslem3  15820  2lgsoddprmlem1  15824  usgrexmpldifpr  16088  ex-an  16255  ex-fl  16257  ex-exp  16259  bdbm1.3ii  16422  subctctexmid  16537