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  1201  sbequilem  1886  unssi  3382  ssini  3430  bm1.3ii  4210  epelg  4387  pwnex  4546  onsucelsucexmid  4628  elvv  4788  relopabiv  4853  funpr  5382  mpov  6111  caovcom  6180  th3q  6809  endisj  7008  phplem2  7039  ssfiexmidt  7065  addnnnq0  7669  mulnnnq0  7670  nqprxx  7766  addsrpr  7965  mulsrpr  7966  recidpirq  8078  apreim  8783  aptap  8830  mulcanapi  8847  div1  8883  recdivap  8898  divdivap1  8903  divdivap2  8904  divassapi  8948  divdirapi  8949  div23api  8950  div11api  8951  divmuldivapi  8952  divmul13api  8953  divadddivapi  8954  divdivdivapi  8955  lemulge11  9046  negiso  9135  2cnne0  9353  2rene0  9354  1mhlfehlf  9362  halfpm6th  9364  2halves  9373  halfaddsub  9378  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  3halfnz  9577  nneoor  9582  zeo  9585  divlt1lt  9959  divle1le  9960  nnledivrp  10001  fz0to4untppr  10359  2tnp1ge0ge0  10562  frecfzennn  10689  xnn0nnen  10700  fxnn0nninf  10702  expge1  10839  faclbnd2  11005  4bc2eq6  11037  cjreb  11428  sqrt2gt1lt2  11611  amgm2  11680  xrnegiso  11824  ege2le3  12234  efi4p  12280  efival  12295  cosmul  12308  sin01bnd  12320  cos01bnd  12321  cos1bnd  12322  cos2bnd  12323  sin01gt0  12325  cos01gt0  12326  sin02gt0  12327  sincos2sgn  12329  sin4lt0  12330  egt2lt3  12343  3dvdsdec  12428  3dvds2dec  12429  odd2np1  12436  oddge22np1  12444  ltoddhalfle  12456  halfleoddlt  12457  nno  12469  ndvdsi  12496  flodddiv4  12499  flodddiv4lt  12501  flodddiv4t2lthalf  12502  bitsp1o  12516  3lcm2e6woprm  12660  6lcm4e12  12661  pcrec  12883  ennnfonelemj0  13024  structfn  13103  ndxslid  13109  strleun  13189  slotsdifipndx  13260  slotsdifplendx  13295  slotsdifdsndx  13310  slotsdifunifndx  13317  cnfld1  14589  expghmap  14624  isbasis3g  14773  bl2in  15130  dveflem  15453  cosz12  15507  sinhalfpilem  15518  ptolemy  15551  sincosq1lem  15552  sincosq4sgn  15556  sinq12gt0  15557  cosq23lt0  15560  coseq00topi  15562  coseq0negpitopi  15563  tangtx  15565  sincos4thpi  15567  sincos6thpi  15569  sincos3rdpi  15570  pigt3  15571  coskpi  15575  cos02pilt1  15578  2logb9irrALT  15701  lgsdir2lem1  15760  1lgs  15775  gausslemma2dlem0c  15783  gausslemma2dlem0d  15784  gausslemma2dlem1a  15790  gausslemma2dlem2  15794  gausslemma2dlem3  15795  lgsquad2lem2  15814  2lgslem1a1  15818  2lgslem1a2  15819  2lgslem1c  15822  2lgslem3  15833  2lgsoddprmlem1  15837  usgrexmpldifpr  16103  uhgrsubgrself  16120  ex-an  16336  ex-fl  16338  ex-exp  16340  bdbm1.3ii  16507  subctctexmid  16622