Theorem pm3.2i 267

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-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mp4an  419  pm4.87  525  biijust  608  3pm3.2i  1124  sbequilem  1773  unssi  3190  ssini  3238  bm1.3ii  3981  epelg  4141  pwnex  4299  onsucelsucexmid  4374  elvv  4529  funpr  5100  mpt2v  5776  caovcom  5840  th3q  6437  endisj  6620  phplem2  6649  addnnnq0  7105  mulnnnq0  7106  nqprxx  7202  addsrpr  7388  mulsrpr  7389  recidpirq  7492  apreim  8177  mulcanapi  8233  div1  8267  recdivap  8282  divdivap1  8287  divdivap2  8288  divassapi  8332  divdirapi  8333  div23api  8334  div11api  8335  divmuldivapi  8336  divmul13api  8337  divadddivapi  8338  divdivdivapi  8339  lemulge11  8424  negiso  8513  2cnne0  8723  2rene0  8724  1mhlfehlf  8732  halfpm6th  8734  2halves  8743  halfaddsub  8748  avglt1  8752  avglt2  8753  div4p1lem1div2  8767  3halfnz  8942  nneoor  8947  zeo  8950  divlt1lt  9300  divle1le  9301  nnledivrp  9336  2tnp1ge0ge0  9857  frecfzennn  9982  fxnn0nninf  9993  expge1  10123  faclbnd2  10281  4bc2eq6  10313  cjreb  10431  sqrt2gt1lt2  10613  amgm2  10682  xrnegiso  10821  ege2le3  11126  efi4p  11173  efival  11188  cosmul  11201  sin01bnd  11213  cos01bnd  11214  cos1bnd  11215  cos2bnd  11216  sin01gt0  11217  cos01gt0  11218  sin02gt0  11219  sincos2sgn  11221  sin4lt0  11222  egt2lt3  11232  3dvdsdec  11308  3dvds2dec  11309  odd2np1  11316  oddge22np1  11324  ltoddhalfle  11336  halfleoddlt  11337  nno  11349  ndvdsi  11376  flodddiv4  11377  flodddiv4lt  11379  flodddiv4t2lthalf  11380  3lcm2e6woprm  11511  6lcm4e12  11512  structfn  11678  ndxslid  11684  strleun  11748  isbasis3g  11912  bl2in  12205  ex-an  12374  ex-fl  12376  ex-exp  12378  bdbm1.3ii  12506