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  1201  sbequilem  1886  unssi  3382  ssini  3430  bm1.3ii  4210  epelg  4387  pwnex  4546  onsucelsucexmid  4628  elvv  4788  relopabiv  4853  funpr  5382  mpov  6111  caovcom  6180  th3q  6809  endisj  7008  phplem2  7039  ssfiexmidt  7065  addnnnq0  7669  mulnnnq0  7670  nqprxx  7766  addsrpr  7965  mulsrpr  7966  recidpirq  8078  apreim  8783  aptap  8830  mulcanapi  8847  div1  8883  recdivap  8898  divdivap1  8903  divdivap2  8904  divassapi  8948  divdirapi  8949  div23api  8950  div11api  8951  divmuldivapi  8952  divmul13api  8953  divadddivapi  8954  divdivdivapi  8955  lemulge11  9046  negiso  9135  2cnne0  9353  2rene0  9354  1mhlfehlf  9362  halfpm6th  9364  2halves  9373  halfaddsub  9378  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  3halfnz  9577  nneoor  9582  zeo  9585  divlt1lt  9959  divle1le  9960  nnledivrp  10001  fz0to4untppr  10359  2tnp1ge0ge0  10562  frecfzennn  10689  xnn0nnen  10700  fxnn0nninf  10702  expge1  10839  faclbnd2  11005  4bc2eq6  11037  cjreb  11444  sqrt2gt1lt2  11627  amgm2  11696  xrnegiso  11840  ege2le3  12250  efi4p  12296  efival  12311  cosmul  12324  sin01bnd  12336  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  sincos2sgn  12345  sin4lt0  12346  egt2lt3  12359  3dvdsdec  12444  3dvds2dec  12445  odd2np1  12452  oddge22np1  12460  ltoddhalfle  12472  halfleoddlt  12473  nno  12485  ndvdsi  12512  flodddiv4  12515  flodddiv4lt  12517  flodddiv4t2lthalf  12518  bitsp1o  12532  3lcm2e6woprm  12676  6lcm4e12  12677  pcrec  12899  ennnfonelemj0  13040  structfn  13119  ndxslid  13125  strleun  13205  slotsdifipndx  13276  slotsdifplendx  13311  slotsdifdsndx  13326  slotsdifunifndx  13333  cnfld1  14605  expghmap  14640  isbasis3g  14789  bl2in  15146  dveflem  15469  cosz12  15523  sinhalfpilem  15534  ptolemy  15567  sincosq1lem  15568  sincosq4sgn  15572  sinq12gt0  15573  cosq23lt0  15576  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  sincos6thpi  15585  sincos3rdpi  15586  pigt3  15587  coskpi  15591  cos02pilt1  15594  2logb9irrALT  15717  lgsdir2lem1  15776  1lgs  15791  gausslemma2dlem0c  15799  gausslemma2dlem0d  15800  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquad2lem2  15830  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1c  15838  2lgslem3  15849  2lgsoddprmlem1  15853  usgrexmpldifpr  16119  uhgrsubgrself  16136  konigsberglem1  16358  ex-an  16366  ex-fl  16368  ex-exp  16370  bdbm1.3ii  16537  subctctexmid  16652  qdiff  16704