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  7816  mulnnnq0  7817  nqprxx  7913  addsrpr  8112  mulsrpr  8113  recidpirq  8225  apreim  8932  aptap  8979  mulcanapi  8996  div1  9034  recdivap  9049  divdivap1  9054  divdivap2  9055  divassapi  9099  divdirapi  9100  div23api  9101  div11api  9102  divmuldivapi  9103  divmul13api  9104  divadddivapi  9105  divdivdivapi  9106  lemulge11  9197  negiso  9286  2cnne0  9516  2rene0  9517  1mhlfehlf  9525  halfpm6th  9527  2halves  9536  halfaddsub  9541  avglt1  9546  avglt2  9547  div4p1lem1div2  9561  3halfnz  9745  nneoor  9750  zeo  9753  divlt1lt  10127  divle1le  10128  nnledivrp  10169  fz0to4untppr  10533  2tnp1ge0ge0  10738  frecfzennn  10865  xnn0nnen  10876  fxnn0nninf  10878  expge1  11015  faclbnd2  11182  4bc2eq6  11215  cjreb  11633  sqrt2gt1lt2  11817  amgm2  11886  xrnegiso  12030  ege2le3  12440  efi4p  12486  efival  12501  cosmul  12514  sin01bnd  12526  cos01bnd  12527  cos1bnd  12528  cos2bnd  12529  sin01gt0  12531  cos01gt0  12532  sin02gt0  12533  sincos2sgn  12535  sin4lt0  12536  egt2lt3  12549  3dvdsdec  12634  3dvds2dec  12635  odd2np1  12642  oddge22np1  12650  ltoddhalfle  12662  halfleoddlt  12663  nno  12675  ndvdsi  12702  flodddiv4  12705  flodddiv4lt  12707  flodddiv4t2lthalf  12708  bitsp1o  12722  3lcm2e6woprm  12866  6lcm4e12  12867  pcrec  13089  ballotfilemonn  13223  ballotfilemth  13283  ennnfonelemj0  13294  structfn  13373  ndxslid  13379  strleun  13460  slotsdifipndx  13531  slotsdifplendx  13566  slotsdifdsndx  13581  slotsdifunifndx  13588  cnfld1  14911  expghmap  14944  isbasis3g  15149  bl2in  15506  dveflem  15829  cosz12  15884  sinhalfpilem  15895  ptolemy  15928  sincosq1lem  15929  sincosq4sgn  15933  sinq12gt0  15934  cosq23lt0  15937  coseq00topi  15939  coseq0negpitopi  15940  tangtx  15942  sincos4thpi  15944  sincos6thpi  15946  sincos3rdpi  15947  pigt3  15948  coskpi  15952  cos02pilt1  15955  2logb9irrALT  16082  log2tlbndlog2  16088  log2ublem1  16089  log2ublog2  16092  bcmono  16124  bclbnd  16127  lgsdir2lem1  16159  1lgs  16174  gausslemma2dlem0c  16182  gausslemma2dlem0d  16183  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  gausslemma2dlem3  16194  lgsquad2lem2  16213  2lgslem1a1  16217  2lgslem1a2  16218  2lgslem1c  16221  2lgslem3  16232  2lgsoddprmlem1  16236  usgrexmpldifpr  16502  uhgrsubgrself  16519  konigsberglem1  16741  ex-an  16749  ex-fl  16751  ex-exp  16753  bdbm1.3ii  16929  subctctexmid  17042  wexmiddifxy  17058  qdiff  17110