Theorem pm3.2i 266

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 137	. 2 |- ( ph -> ( ps -> ( ph /\ ps ) ) )
4	1, 2, 3	mp2 16	1 |- ( ph /\ ps )

Syntax hints:   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  mp4an  417  pm4.87  523  biijust  602  3pm3.2i  1116  sbequilem  1759  unssi  3147  ssini  3189  bm1.3ii  3899  epelg  4045  onsucelsucexmid  4273  elvv  4420  funpr  4971  mpt2v  5614  caovcom  5678  th3q  6234  endisj  6321  phplem2  6339  addnnnq0  6639  mulnnnq0  6640  nqprxx  6736  addsrpr  6922  mulsrpr  6923  recidpirq  7026  apreim  7703  mulcanapi  7757  div1  7791  recdivap  7806  divdivap1  7811  divdivap2  7812  divassapi  7856  divdirapi  7857  div23api  7858  div11api  7859  divmuldivapi  7860  divmul13api  7861  divadddivapi  7862  divdivdivapi  7863  lemulge11  7944  negiso  8033  2cnne0  8240  2rene0  8241  1mhlfehlf  8249  halfpm6th  8251  2halves  8260  halfaddsub  8265  avglt1  8269  avglt2  8270  div4p1lem1div2  8284  3halfnz  8444  nneoor  8449  zeo  8452  divlt1lt  8801  divle1le  8802  nnledivrp  8837  2tnp1ge0ge0  9303  frecfzennn  9419  expge1  9513  faclbnd2  9669  4bc2eq6  9701  cjreb  9753  sqrt2gt1lt2  9935  amgm2  10004  3dvdsdec  10264  3dvds2dec  10265  odd2np1  10272  oddge22np1  10281  ltoddhalfle  10293  halfleoddlt  10294  nno  10306  ndvdsi  10333  flodddiv4  10334  flodddiv4lt  10336  flodddiv4t2lthalf  10337  3lcm2e6woprm  10468  6lcm4e12  10469  ex-an  10561  ex-fl  10563  bdbm1.3ii  10682