Theorem pm3.2i 272

Description: Infer conjunction of premises. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
pm3.2i.1	⊢ 𝜑
pm3.2i.2	⊢ 𝜓

Assertion

Ref	Expression
pm3.2i	⊢ (𝜑 ∧ 𝜓)

Proof of Theorem pm3.2i

Step	Hyp	Ref	Expression
1		pm3.2i.1	. 2 ⊢ 𝜑
2		pm3.2i.2	. 2 ⊢ 𝜓
3		pm3.2 139	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ∧ 𝜓)

This proof depends on syntax axioms:   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  mp4an  431  pm4.87  563  biijust  650  3pm3.2i  1206  sbequilem  1891  unssi  3404  ssini  3454  bm1.3ii  4254  epelg  4435  pwnex  4595  onsucelsucexmid  4677  elvv  4837  relopabiv  4903  funpr  5433  mpov  6178  caovcom  6247  th3q  6914  endisj  7122  phplem2  7154  ssfiexmidt  7180  addnnnq0  7817  mulnnnq0  7818  nqprxx  7914  addsrpr  8113  mulsrpr  8114  recidpirq  8226  apreim  8934  aptap  8981  mulcanapi  8998  div1  9036  recdivap  9051  divdivap1  9056  divdivap2  9057  divassapi  9101  divdirapi  9102  div23api  9103  div11api  9104  divmuldivapi  9105  divmul13api  9106  divadddivapi  9107  divdivdivapi  9108  lemulge11  9199  negiso  9288  2cnne0  9519  2rene0  9520  1mhlfehlf  9528  halfpm6th  9530  2halves  9539  halfaddsub  9544  avglt1  9549  avglt2  9550  div4p1lem1div2  9564  3halfnz  9748  nneoor  9753  zeo  9756  divlt1lt  10136  divle1le  10137  nnledivrp  10178  fz0to4untppr  10542  2tnp1ge0ge0  10751  frecfzennn  10878  xnn0nnen  10889  fxnn0nninf  10891  expge1  11028  faclbnd2  11196  4bc2eq6  11229  cjreb  11647  sqrt2gt1lt2  11831  amgm2  11901  xrnegiso  12047  ege2le3  12457  efi4p  12503  efival  12518  cosmul  12531  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  sincos2sgn  12552  sin4lt0  12553  egt2lt3  12566  3dvdsdec  12651  3dvds2dec  12652  odd2np1  12659  oddge22np1  12667  ltoddhalfle  12679  halfleoddlt  12680  nno  12692  ndvdsi  12719  flodddiv4  12722  flodddiv4lt  12724  flodddiv4t2lthalf  12725  bitsp1o  12739  3lcm2e6woprm  12883  6lcm4e12  12884  pcrec  13110  ballotfilemonn  13273  ballotfilemth  13333  ennnfonelemj0  13344  structfn  13423  ndxslid  13429  strleun  13511  slotsdifipndx  13582  slotsdifplendx  13617  slotsdifdsndx  13632  slotsdifunifndx  13639  cnfld1  14993  expghmap  15026  isbasis3g  15238  bl2in  15595  dveflem  15918  cosz12  15973  sinhalfpilem  15984  ptolemy  16017  sincosq1lem  16018  sincosq4sgn  16022  sinq12gt0  16023  cosq23lt0  16026  coseq00topi  16028  coseq0negpitopi  16029  tangtx  16031  sincos4thpi  16033  sincos6thpi  16035  sincos3rdpi  16036  pigt3  16037  coskpi  16041  cos02pilt1  16045  2logb9irrALT  16176  log2tlbndlog2  16186  log2ublem1  16187  log2ublog2  16190  ppiublem1  16257  ppiublem2  16258  ppiqub  16259  chtublem  16261  chtqub  16262  bcmono  16270  bclbnd  16273  bpos1lem  16275  bposlem1  16277  bposlem2  16278  bposlem3  16279  bposlem4  16280  bposlem5  16281  bposlem6  16282  bposlem7  16283  bposlem8  16284  bposlem9  16285  lgsdir2lem1  16318  1lgs  16333  gausslemma2dlem0c  16341  gausslemma2dlem0d  16342  gausslemma2dlem1a  16348  gausslemma2dlem2  16352  gausslemma2dlem3  16353  lgsquad2lem2  16372  2lgslem1a1  16376  2lgslem1a2  16377  2lgslem1c  16380  2lgslem3  16391  2lgsoddprmlem1  16395  usgrexmpldifpr  16661  uhgrsubgrself  16678  konigsberglem1  16900  ex-an  16908  ex-fl  16910  ex-exp  16912  bdbm1.3ii  17088  subctctexmid  17201  wexmiddifxy  17217  qdiff  17270