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  1852  unssi  3339  ssini  3387  bm1.3ii  4155  epelg  4326  pwnex  4485  onsucelsucexmid  4567  elvv  4726  relopabiv  4790  funpr  5311  mpov  6016  caovcom  6085  th3q  6708  endisj  6892  phplem2  6923  addnnnq0  7533  mulnnnq0  7534  nqprxx  7630  addsrpr  7829  mulsrpr  7830  recidpirq  7942  apreim  8647  aptap  8694  mulcanapi  8711  div1  8747  recdivap  8762  divdivap1  8767  divdivap2  8768  divassapi  8812  divdirapi  8813  div23api  8814  div11api  8815  divmuldivapi  8816  divmul13api  8817  divadddivapi  8818  divdivdivapi  8819  lemulge11  8910  negiso  8999  2cnne0  9217  2rene0  9218  1mhlfehlf  9226  halfpm6th  9228  2halves  9237  halfaddsub  9242  avglt1  9247  avglt2  9248  div4p1lem1div2  9262  3halfnz  9440  nneoor  9445  zeo  9448  divlt1lt  9816  divle1le  9817  nnledivrp  9858  fz0to4untppr  10216  2tnp1ge0ge0  10408  frecfzennn  10535  xnn0nnen  10546  fxnn0nninf  10548  expge1  10685  faclbnd2  10851  4bc2eq6  10883  cjreb  11048  sqrt2gt1lt2  11231  amgm2  11300  xrnegiso  11444  ege2le3  11853  efi4p  11899  efival  11914  cosmul  11927  sin01bnd  11939  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  sincos2sgn  11948  sin4lt0  11949  egt2lt3  11962  3dvdsdec  12047  3dvds2dec  12048  odd2np1  12055  oddge22np1  12063  ltoddhalfle  12075  halfleoddlt  12076  nno  12088  ndvdsi  12115  flodddiv4  12118  flodddiv4lt  12120  flodddiv4t2lthalf  12121  bitsp1o  12135  3lcm2e6woprm  12279  6lcm4e12  12280  pcrec  12502  ennnfonelemj0  12643  structfn  12722  ndxslid  12728  strleun  12807  slotsdifipndx  12877  slotsdifplendx  12912  slotsdifdsndx  12927  slotsdifunifndx  12934  cnfld1  14204  expghmap  14239  isbasis3g  14366  bl2in  14723  dveflem  15046  cosz12  15100  sinhalfpilem  15111  ptolemy  15144  sincosq1lem  15145  sincosq4sgn  15149  sinq12gt0  15150  cosq23lt0  15153  coseq00topi  15155  coseq0negpitopi  15156  tangtx  15158  sincos4thpi  15160  sincos6thpi  15162  sincos3rdpi  15163  pigt3  15164  coskpi  15168  cos02pilt1  15171  2logb9irrALT  15294  lgsdir2lem1  15353  1lgs  15368  gausslemma2dlem0c  15376  gausslemma2dlem0d  15377  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem3  15388  lgsquad2lem2  15407  2lgslem1a1  15411  2lgslem1a2  15412  2lgslem1c  15415  2lgslem3  15426  2lgsoddprmlem1  15430  ex-an  15453  ex-fl  15455  ex-exp  15457  bdbm1.3ii  15621  subctctexmid  15731