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  431  pm4.87  563  biijust  650  3pm3.2i  1206  sbequilem  1891  unssi  3404  ssini  3454  bm1.3ii  4249  epelg  4430  pwnex  4590  onsucelsucexmid  4672  elvv  4832  relopabiv  4898  funpr  5428  mpov  6168  caovcom  6237  th3q  6904  endisj  7112  phplem2  7144  ssfiexmidt  7170  addnnnq0  7806  mulnnnq0  7807  nqprxx  7903  addsrpr  8102  mulsrpr  8103  recidpirq  8215  apreim  8921  aptap  8968  mulcanapi  8985  div1  9023  recdivap  9038  divdivap1  9043  divdivap2  9044  divassapi  9088  divdirapi  9089  div23api  9090  div11api  9091  divmuldivapi  9092  divmul13api  9093  divadddivapi  9094  divdivdivapi  9095  lemulge11  9186  negiso  9275  2cnne0  9493  2rene0  9494  1mhlfehlf  9502  halfpm6th  9504  2halves  9513  halfaddsub  9518  avglt1  9523  avglt2  9524  div4p1lem1div2  9538  3halfnz  9722  nneoor  9727  zeo  9730  divlt1lt  10104  divle1le  10105  nnledivrp  10146  fz0to4untppr  10509  2tnp1ge0ge0  10714  frecfzennn  10841  xnn0nnen  10852  fxnn0nninf  10854  expge1  10991  faclbnd2  11158  4bc2eq6  11191  cjreb  11609  sqrt2gt1lt2  11793  amgm2  11862  xrnegiso  12006  ege2le3  12416  efi4p  12462  efival  12477  cosmul  12490  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  sincos2sgn  12511  sin4lt0  12512  egt2lt3  12525  3dvdsdec  12610  3dvds2dec  12611  odd2np1  12618  oddge22np1  12626  ltoddhalfle  12638  halfleoddlt  12639  nno  12651  ndvdsi  12678  flodddiv4  12681  flodddiv4lt  12683  flodddiv4t2lthalf  12684  bitsp1o  12698  3lcm2e6woprm  12842  6lcm4e12  12843  pcrec  13065  ballotfilemonn  13199  ballotfilemth  13259  ennnfonelemj0  13270  structfn  13349  ndxslid  13355  strleun  13435  slotsdifipndx  13506  slotsdifplendx  13541  slotsdifdsndx  13556  slotsdifunifndx  13563  cnfld1  14881  expghmap  14914  isbasis3g  15070  bl2in  15427  dveflem  15750  cosz12  15804  sinhalfpilem  15815  ptolemy  15848  sincosq1lem  15849  sincosq4sgn  15853  sinq12gt0  15854  cosq23lt0  15857  coseq00topi  15859  coseq0negpitopi  15860  tangtx  15862  sincos4thpi  15864  sincos6thpi  15866  sincos3rdpi  15867  pigt3  15868  coskpi  15872  cos02pilt1  15875  2logb9irrALT  15999  lgsdir2lem1  16061  1lgs  16076  gausslemma2dlem0c  16084  gausslemma2dlem0d  16085  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem3  16096  lgsquad2lem2  16115  2lgslem1a1  16119  2lgslem1a2  16120  2lgslem1c  16123  2lgslem3  16134  2lgsoddprmlem1  16138  usgrexmpldifpr  16404  uhgrsubgrself  16421  konigsberglem1  16643  ex-an  16651  ex-fl  16653  ex-exp  16655  bdbm1.3ii  16831  subctctexmid  16944  qdiff  17003