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  424  pm4.87  547  biijust  631  3pm3.2i  1165  sbequilem  1826  unssi  3296  ssini  3344  bm1.3ii  4102  epelg  4267  pwnex  4426  onsucelsucexmid  4506  elvv  4665  funpr  5239  mpov  5928  caovcom  5995  th3q  6602  endisj  6786  phplem2  6815  addnnnq0  7386  mulnnnq0  7387  nqprxx  7483  addsrpr  7682  mulsrpr  7683  recidpirq  7795  apreim  8497  mulcanapi  8560  div1  8595  recdivap  8610  divdivap1  8615  divdivap2  8616  divassapi  8660  divdirapi  8661  div23api  8662  div11api  8663  divmuldivapi  8664  divmul13api  8665  divadddivapi  8666  divdivdivapi  8667  lemulge11  8757  negiso  8846  2cnne0  9062  2rene0  9063  1mhlfehlf  9071  halfpm6th  9073  2halves  9082  halfaddsub  9087  avglt1  9091  avglt2  9092  div4p1lem1div2  9106  3halfnz  9284  nneoor  9289  zeo  9292  divlt1lt  9656  divle1le  9657  nnledivrp  9698  fz0to4untppr  10055  2tnp1ge0ge0  10232  frecfzennn  10357  fxnn0nninf  10369  expge1  10488  faclbnd2  10651  4bc2eq6  10683  cjreb  10804  sqrt2gt1lt2  10987  amgm2  11056  xrnegiso  11199  ege2le3  11608  efi4p  11654  efival  11669  cosmul  11682  sin01bnd  11694  cos01bnd  11695  cos1bnd  11696  cos2bnd  11697  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  sincos2sgn  11702  sin4lt0  11703  egt2lt3  11716  3dvdsdec  11798  3dvds2dec  11799  odd2np1  11806  oddge22np1  11814  ltoddhalfle  11826  halfleoddlt  11827  nno  11839  ndvdsi  11866  flodddiv4  11867  flodddiv4lt  11869  flodddiv4t2lthalf  11870  3lcm2e6woprm  12014  6lcm4e12  12015  pcrec  12236  ennnfonelemj0  12330  structfn  12409  ndxslid  12415  strleun  12479  isbasis3g  12644  bl2in  13003  dveflem  13287  cosz12  13301  sinhalfpilem  13312  ptolemy  13345  sincosq1lem  13346  sincosq4sgn  13350  sinq12gt0  13351  cosq23lt0  13354  coseq00topi  13356  coseq0negpitopi  13357  tangtx  13359  sincos4thpi  13361  sincos6thpi  13363  sincos3rdpi  13364  pigt3  13365  coskpi  13369  cos02pilt1  13372  2logb9irrALT  13492  lgsdir2lem1  13529  1lgs  13544  ex-an  13564  ex-fl  13566  ex-exp  13568  bdbm1.3ii  13733  subctctexmid  13841