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  642  3pm3.2i  1177  sbequilem  1860  unssi  3347  ssini  3395  bm1.3ii  4164  epelg  4335  pwnex  4494  onsucelsucexmid  4576  elvv  4735  relopabiv  4799  funpr  5320  mpov  6025  caovcom  6094  th3q  6717  endisj  6901  phplem2  6932  addnnnq0  7544  mulnnnq0  7545  nqprxx  7641  addsrpr  7840  mulsrpr  7841  recidpirq  7953  apreim  8658  aptap  8705  mulcanapi  8722  div1  8758  recdivap  8773  divdivap1  8778  divdivap2  8779  divassapi  8823  divdirapi  8824  div23api  8825  div11api  8826  divmuldivapi  8827  divmul13api  8828  divadddivapi  8829  divdivdivapi  8830  lemulge11  8921  negiso  9010  2cnne0  9228  2rene0  9229  1mhlfehlf  9237  halfpm6th  9239  2halves  9248  halfaddsub  9253  avglt1  9258  avglt2  9259  div4p1lem1div2  9273  3halfnz  9452  nneoor  9457  zeo  9460  divlt1lt  9828  divle1le  9829  nnledivrp  9870  fz0to4untppr  10228  2tnp1ge0ge0  10425  frecfzennn  10552  xnn0nnen  10563  fxnn0nninf  10565  expge1  10702  faclbnd2  10868  4bc2eq6  10900  cjreb  11096  sqrt2gt1lt2  11279  amgm2  11348  xrnegiso  11492  ege2le3  11901  efi4p  11947  efival  11962  cosmul  11975  sin01bnd  11987  cos01bnd  11988  cos1bnd  11989  cos2bnd  11990  sin01gt0  11992  cos01gt0  11993  sin02gt0  11994  sincos2sgn  11996  sin4lt0  11997  egt2lt3  12010  3dvdsdec  12095  3dvds2dec  12096  odd2np1  12103  oddge22np1  12111  ltoddhalfle  12123  halfleoddlt  12124  nno  12136  ndvdsi  12163  flodddiv4  12166  flodddiv4lt  12168  flodddiv4t2lthalf  12169  bitsp1o  12183  3lcm2e6woprm  12327  6lcm4e12  12328  pcrec  12550  ennnfonelemj0  12691  structfn  12770  ndxslid  12776  strleun  12855  slotsdifipndx  12925  slotsdifplendx  12960  slotsdifdsndx  12975  slotsdifunifndx  12982  cnfld1  14252  expghmap  14287  isbasis3g  14436  bl2in  14793  dveflem  15116  cosz12  15170  sinhalfpilem  15181  ptolemy  15214  sincosq1lem  15215  sincosq4sgn  15219  sinq12gt0  15220  cosq23lt0  15223  coseq00topi  15225  coseq0negpitopi  15226  tangtx  15228  sincos4thpi  15230  sincos6thpi  15232  sincos3rdpi  15233  pigt3  15234  coskpi  15238  cos02pilt1  15241  2logb9irrALT  15364  lgsdir2lem1  15423  1lgs  15438  gausslemma2dlem0c  15446  gausslemma2dlem0d  15447  gausslemma2dlem1a  15453  gausslemma2dlem2  15457  gausslemma2dlem3  15458  lgsquad2lem2  15477  2lgslem1a1  15481  2lgslem1a2  15482  2lgslem1c  15485  2lgslem3  15496  2lgsoddprmlem1  15500  ex-an  15523  ex-fl  15525  ex-exp  15527  bdbm1.3ii  15691  subctctexmid  15801