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  1202  sbequilem  1887  unssi  3394  ssini  3444  bm1.3ii  4231  epelg  4411  pwnex  4570  onsucelsucexmid  4652  elvv  4812  relopabiv  4878  funpr  5408  mpov  6143  caovcom  6212  th3q  6874  endisj  7075  phplem2  7107  ssfiexmidt  7133  addnnnq0  7764  mulnnnq0  7765  nqprxx  7861  addsrpr  8060  mulsrpr  8061  recidpirq  8173  apreim  8877  aptap  8924  mulcanapi  8941  div1  8977  recdivap  8992  divdivap1  8997  divdivap2  8998  divassapi  9042  divdirapi  9043  div23api  9044  div11api  9045  divmuldivapi  9046  divmul13api  9047  divadddivapi  9048  divdivdivapi  9049  lemulge11  9140  negiso  9229  2cnne0  9447  2rene0  9448  1mhlfehlf  9456  halfpm6th  9458  2halves  9467  halfaddsub  9472  avglt1  9477  avglt2  9478  div4p1lem1div2  9492  3halfnz  9675  nneoor  9680  zeo  9683  divlt1lt  10057  divle1le  10058  nnledivrp  10099  fz0to4untppr  10458  2tnp1ge0ge0  10661  frecfzennn  10788  xnn0nnen  10799  fxnn0nninf  10801  expge1  10938  faclbnd2  11104  4bc2eq6  11137  cjreb  11551  sqrt2gt1lt2  11734  amgm2  11803  xrnegiso  11947  ege2le3  12357  efi4p  12403  efival  12418  cosmul  12431  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  sincos2sgn  12452  sin4lt0  12453  egt2lt3  12466  3dvdsdec  12551  3dvds2dec  12552  odd2np1  12559  oddge22np1  12567  ltoddhalfle  12579  halfleoddlt  12580  nno  12592  ndvdsi  12619  flodddiv4  12622  flodddiv4lt  12624  flodddiv4t2lthalf  12625  bitsp1o  12639  3lcm2e6woprm  12783  6lcm4e12  12784  pcrec  13006  ballotfilemonn  13140  ennnfonelemj0  13152  structfn  13231  ndxslid  13237  strleun  13317  slotsdifipndx  13388  slotsdifplendx  13423  slotsdifdsndx  13438  slotsdifunifndx  13445  cnfld1  14720  expghmap  14755  isbasis3g  14911  bl2in  15268  dveflem  15591  cosz12  15645  sinhalfpilem  15656  ptolemy  15689  sincosq1lem  15690  sincosq4sgn  15694  sinq12gt0  15695  cosq23lt0  15698  coseq00topi  15700  coseq0negpitopi  15701  tangtx  15703  sincos4thpi  15705  sincos6thpi  15707  sincos3rdpi  15708  pigt3  15709  coskpi  15713  cos02pilt1  15716  2logb9irrALT  15839  lgsdir2lem1  15901  1lgs  15916  gausslemma2dlem0c  15924  gausslemma2dlem0d  15925  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  lgsquad2lem2  15955  2lgslem1a1  15959  2lgslem1a2  15960  2lgslem1c  15963  2lgslem3  15974  2lgsoddprmlem1  15978  usgrexmpldifpr  16244  uhgrsubgrself  16261  konigsberglem1  16483  ex-an  16491  ex-fl  16493  ex-exp  16495  bdbm1.3ii  16661  subctctexmid  16774  qdiff  16833