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  418  pm4.87  524  biijust  603  3pm3.2i  1119  sbequilem  1763  unssi  3164  ssini  3212  bm1.3ii  3933  epelg  4089  onsucelsucexmid  4317  elvv  4466  funpr  5027  mpt2v  5688  caovcom  5752  th3q  6342  endisj  6485  phplem2  6514  addnnnq0  6944  mulnnnq0  6945  nqprxx  7041  addsrpr  7227  mulsrpr  7228  recidpirq  7331  apreim  8013  mulcanapi  8067  div1  8101  recdivap  8116  divdivap1  8121  divdivap2  8122  divassapi  8166  divdirapi  8167  div23api  8168  div11api  8169  divmuldivapi  8170  divmul13api  8171  divadddivapi  8172  divdivdivapi  8173  lemulge11  8254  negiso  8343  2cnne0  8550  2rene0  8551  1mhlfehlf  8559  halfpm6th  8561  2halves  8570  halfaddsub  8575  avglt1  8579  avglt2  8580  div4p1lem1div2  8594  3halfnz  8768  nneoor  8773  zeo  8776  divlt1lt  9125  divle1le  9126  nnledivrp  9161  2tnp1ge0ge0  9628  frecfzennn  9753  fxnn0nninf  9764  expge1  9882  faclbnd2  10038  4bc2eq6  10070  cjreb  10187  sqrt2gt1lt2  10369  amgm2  10438  3dvdsdec  10731  3dvds2dec  10732  odd2np1  10739  oddge22np1  10747  ltoddhalfle  10759  halfleoddlt  10760  nno  10772  ndvdsi  10799  flodddiv4  10800  flodddiv4lt  10802  flodddiv4t2lthalf  10803  3lcm2e6woprm  10934  6lcm4e12  10935  ex-an  11080  ex-fl  11082  bdbm1.3ii  11211