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  1886  unssi  3384  ssini  3432  bm1.3ii  4215  epelg  4393  pwnex  4552  onsucelsucexmid  4634  elvv  4794  relopabiv  4859  funpr  5389  mpov  6121  caovcom  6190  th3q  6852  endisj  7051  phplem2  7082  ssfiexmidt  7108  addnnnq0  7712  mulnnnq0  7713  nqprxx  7809  addsrpr  8008  mulsrpr  8009  recidpirq  8121  apreim  8825  aptap  8872  mulcanapi  8889  div1  8925  recdivap  8940  divdivap1  8945  divdivap2  8946  divassapi  8990  divdirapi  8991  div23api  8992  div11api  8993  divmuldivapi  8994  divmul13api  8995  divadddivapi  8996  divdivdivapi  8997  lemulge11  9088  negiso  9177  2cnne0  9395  2rene0  9396  1mhlfehlf  9404  halfpm6th  9406  2halves  9415  halfaddsub  9420  avglt1  9425  avglt2  9426  div4p1lem1div2  9440  3halfnz  9621  nneoor  9626  zeo  9629  divlt1lt  10003  divle1le  10004  nnledivrp  10045  fz0to4untppr  10404  2tnp1ge0ge0  10607  frecfzennn  10734  xnn0nnen  10745  fxnn0nninf  10747  expge1  10884  faclbnd2  11050  4bc2eq6  11082  cjreb  11489  sqrt2gt1lt2  11672  amgm2  11741  xrnegiso  11885  ege2le3  12295  efi4p  12341  efival  12356  cosmul  12369  sin01bnd  12381  cos01bnd  12382  cos1bnd  12383  cos2bnd  12384  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  sincos2sgn  12390  sin4lt0  12391  egt2lt3  12404  3dvdsdec  12489  3dvds2dec  12490  odd2np1  12497  oddge22np1  12505  ltoddhalfle  12517  halfleoddlt  12518  nno  12530  ndvdsi  12557  flodddiv4  12560  flodddiv4lt  12562  flodddiv4t2lthalf  12563  bitsp1o  12577  3lcm2e6woprm  12721  6lcm4e12  12722  pcrec  12944  ennnfonelemj0  13085  structfn  13164  ndxslid  13170  strleun  13250  slotsdifipndx  13321  slotsdifplendx  13356  slotsdifdsndx  13371  slotsdifunifndx  13378  cnfld1  14651  expghmap  14686  isbasis3g  14840  bl2in  15197  dveflem  15520  cosz12  15574  sinhalfpilem  15585  ptolemy  15618  sincosq1lem  15619  sincosq4sgn  15623  sinq12gt0  15624  cosq23lt0  15627  coseq00topi  15629  coseq0negpitopi  15630  tangtx  15632  sincos4thpi  15634  sincos6thpi  15636  sincos3rdpi  15637  pigt3  15638  coskpi  15642  cos02pilt1  15645  2logb9irrALT  15768  lgsdir2lem1  15830  1lgs  15845  gausslemma2dlem0c  15853  gausslemma2dlem0d  15854  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquad2lem2  15884  2lgslem1a1  15888  2lgslem1a2  15889  2lgslem1c  15892  2lgslem3  15903  2lgsoddprmlem1  15907  usgrexmpldifpr  16173  uhgrsubgrself  16190  konigsberglem1  16412  ex-an  16420  ex-fl  16422  ex-exp  16424  bdbm1.3ii  16590  subctctexmid  16705  qdiff  16764