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 ⊢ (𝜑 ∧ 𝜓)

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  559  biijust  646  3pm3.2i  1202  sbequilem  1887  unssi  3398  ssini  3448  bm1.3ii  4236  epelg  4416  pwnex  4575  onsucelsucexmid  4657  elvv  4817  relopabiv  4883  funpr  5413  mpov  6151  caovcom  6220  th3q  6887  endisj  7088  phplem2  7120  ssfiexmidt  7146  addnnnq0  7780  mulnnnq0  7781  nqprxx  7877  addsrpr  8076  mulsrpr  8077  recidpirq  8189  apreim  8895  aptap  8942  mulcanapi  8959  div1  8997  recdivap  9012  divdivap1  9017  divdivap2  9018  divassapi  9062  divdirapi  9063  div23api  9064  div11api  9065  divmuldivapi  9066  divmul13api  9067  divadddivapi  9068  divdivdivapi  9069  lemulge11  9160  negiso  9249  2cnne0  9467  2rene0  9468  1mhlfehlf  9476  halfpm6th  9478  2halves  9487  halfaddsub  9492  avglt1  9497  avglt2  9498  div4p1lem1div2  9512  3halfnz  9696  nneoor  9701  zeo  9704  divlt1lt  10078  divle1le  10079  nnledivrp  10120  fz0to4untppr  10483  2tnp1ge0ge0  10688  frecfzennn  10815  xnn0nnen  10826  fxnn0nninf  10828  expge1  10965  faclbnd2  11132  4bc2eq6  11165  cjreb  11579  sqrt2gt1lt2  11762  amgm2  11831  xrnegiso  11975  ege2le3  12385  efi4p  12431  efival  12446  cosmul  12459  sin01bnd  12471  cos01bnd  12472  cos1bnd  12473  cos2bnd  12474  sin01gt0  12476  cos01gt0  12477  sin02gt0  12478  sincos2sgn  12480  sin4lt0  12481  egt2lt3  12494  3dvdsdec  12579  3dvds2dec  12580  odd2np1  12587  oddge22np1  12595  ltoddhalfle  12607  halfleoddlt  12608  nno  12620  ndvdsi  12647  flodddiv4  12650  flodddiv4lt  12652  flodddiv4t2lthalf  12653  bitsp1o  12667  3lcm2e6woprm  12811  6lcm4e12  12812  pcrec  13034  ballotfilemonn  13168  ballotfilemth  13228  ennnfonelemj0  13239  structfn  13318  ndxslid  13324  strleun  13404  slotsdifipndx  13475  slotsdifplendx  13510  slotsdifdsndx  13525  slotsdifunifndx  13532  cnfld1  14849  expghmap  14884  isbasis3g  15040  bl2in  15397  dveflem  15720  cosz12  15774  sinhalfpilem  15785  ptolemy  15818  sincosq1lem  15819  sincosq4sgn  15823  sinq12gt0  15824  cosq23lt0  15827  coseq00topi  15829  coseq0negpitopi  15830  tangtx  15832  sincos4thpi  15834  sincos6thpi  15836  sincos3rdpi  15837  pigt3  15838  coskpi  15842  cos02pilt1  15845  2logb9irrALT  15968  lgsdir2lem1  16030  1lgs  16045  gausslemma2dlem0c  16053  gausslemma2dlem0d  16054  gausslemma2dlem1a  16060  gausslemma2dlem2  16064  gausslemma2dlem3  16065  lgsquad2lem2  16084  2lgslem1a1  16088  2lgslem1a2  16089  2lgslem1c  16092  2lgslem3  16103  2lgsoddprmlem1  16107  usgrexmpldifpr  16373  uhgrsubgrself  16390  konigsberglem1  16612  ex-an  16620  ex-fl  16622  ex-exp  16624  bdbm1.3ii  16800  subctctexmid  16913  qdiff  16972