Theorem pm3.2i 270

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 138	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 103

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

This theorem is referenced by:  mp4an  424  pm4.87  547  biijust  631  3pm3.2i  1164  sbequilem  1825  unssi  3292  ssini  3340  bm1.3ii  4097  epelg  4262  pwnex  4421  onsucelsucexmid  4501  elvv  4660  funpr  5234  mpov  5923  caovcom  5990  th3q  6597  endisj  6781  phplem2  6810  addnnnq0  7381  mulnnnq0  7382  nqprxx  7478  addsrpr  7677  mulsrpr  7678  recidpirq  7790  apreim  8492  mulcanapi  8555  div1  8590  recdivap  8605  divdivap1  8610  divdivap2  8611  divassapi  8655  divdirapi  8656  div23api  8657  div11api  8658  divmuldivapi  8659  divmul13api  8660  divadddivapi  8661  divdivdivapi  8662  lemulge11  8752  negiso  8841  2cnne0  9057  2rene0  9058  1mhlfehlf  9066  halfpm6th  9068  2halves  9077  halfaddsub  9082  avglt1  9086  avglt2  9087  div4p1lem1div2  9101  3halfnz  9279  nneoor  9284  zeo  9287  divlt1lt  9651  divle1le  9652  nnledivrp  9693  fz0to4untppr  10049  2tnp1ge0ge0  10226  frecfzennn  10351  fxnn0nninf  10363  expge1  10482  faclbnd2  10644  4bc2eq6  10676  cjreb  10794  sqrt2gt1lt2  10977  amgm2  11046  xrnegiso  11189  ege2le3  11598  efi4p  11644  efival  11659  cosmul  11672  sin01bnd  11684  cos01bnd  11685  cos1bnd  11686  cos2bnd  11687  sin01gt0  11688  cos01gt0  11689  sin02gt0  11690  sincos2sgn  11692  sin4lt0  11693  egt2lt3  11706  3dvdsdec  11787  3dvds2dec  11788  odd2np1  11795  oddge22np1  11803  ltoddhalfle  11815  halfleoddlt  11816  nno  11828  ndvdsi  11855  flodddiv4  11856  flodddiv4lt  11858  flodddiv4t2lthalf  11859  3lcm2e6woprm  11997  6lcm4e12  11998  pcrec  12217  ennnfonelemj0  12271  structfn  12350  ndxslid  12356  strleun  12420  isbasis3g  12585  bl2in  12944  dveflem  13228  cosz12  13242  sinhalfpilem  13253  ptolemy  13286  sincosq1lem  13287  sincosq4sgn  13291  sinq12gt0  13292  cosq23lt0  13295  coseq00topi  13297  coseq0negpitopi  13298  tangtx  13300  sincos4thpi  13302  sincos6thpi  13304  sincos3rdpi  13305  pigt3  13306  coskpi  13310  cos02pilt1  13313  2logb9irrALT  13433  ex-an  13441  ex-fl  13443  ex-exp  13445  bdbm1.3ii  13608  subctctexmid  13715