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  1849  unssi  3325  ssini  3373  bm1.3ii  4139  epelg  4308  pwnex  4467  onsucelsucexmid  4547  elvv  4706  funpr  5287  mpov  5985  caovcom  6053  th3q  6665  endisj  6849  phplem2  6880  addnnnq0  7477  mulnnnq0  7478  nqprxx  7574  addsrpr  7773  mulsrpr  7774  recidpirq  7886  apreim  8589  aptap  8636  mulcanapi  8653  div1  8689  recdivap  8704  divdivap1  8709  divdivap2  8710  divassapi  8754  divdirapi  8755  div23api  8756  div11api  8757  divmuldivapi  8758  divmul13api  8759  divadddivapi  8760  divdivdivapi  8761  lemulge11  8852  negiso  8941  2cnne0  9157  2rene0  9158  1mhlfehlf  9166  halfpm6th  9168  2halves  9177  halfaddsub  9182  avglt1  9186  avglt2  9187  div4p1lem1div2  9201  3halfnz  9379  nneoor  9384  zeo  9387  divlt1lt  9753  divle1le  9754  nnledivrp  9795  fz0to4untppr  10153  2tnp1ge0ge0  10331  frecfzennn  10456  fxnn0nninf  10468  expge1  10587  faclbnd2  10753  4bc2eq6  10785  cjreb  10906  sqrt2gt1lt2  11089  amgm2  11158  xrnegiso  11301  ege2le3  11710  efi4p  11756  efival  11771  cosmul  11784  sin01bnd  11796  cos01bnd  11797  cos1bnd  11798  cos2bnd  11799  sin01gt0  11800  cos01gt0  11801  sin02gt0  11802  sincos2sgn  11804  sin4lt0  11805  egt2lt3  11818  3dvdsdec  11901  3dvds2dec  11902  odd2np1  11909  oddge22np1  11917  ltoddhalfle  11929  halfleoddlt  11930  nno  11942  ndvdsi  11969  flodddiv4  11970  flodddiv4lt  11972  flodddiv4t2lthalf  11973  3lcm2e6woprm  12117  6lcm4e12  12118  pcrec  12339  ennnfonelemj0  12451  structfn  12530  ndxslid  12536  strleun  12613  slotsdifipndx  12683  slotsdifplendx  12718  slotsdifdsndx  12729  slotsdifunifndx  12736  cnfld1  13872  isbasis3g  13998  bl2in  14355  dveflem  14639  cosz12  14653  sinhalfpilem  14664  ptolemy  14697  sincosq1lem  14698  sincosq4sgn  14702  sinq12gt0  14703  cosq23lt0  14706  coseq00topi  14708  coseq0negpitopi  14709  tangtx  14711  sincos4thpi  14713  sincos6thpi  14715  sincos3rdpi  14716  pigt3  14717  coskpi  14721  cos02pilt1  14724  2logb9irrALT  14844  lgsdir2lem1  14882  1lgs  14897  2lgsoddprmlem1  14906  ex-an  14928  ex-fl  14930  ex-exp  14932  bdbm1.3ii  15096  subctctexmid  15204