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  1165  sbequilem  1826  unssi  3297  ssini  3345  bm1.3ii  4103  epelg  4268  pwnex  4427  onsucelsucexmid  4507  elvv  4666  funpr  5240  mpov  5932  caovcom  5999  th3q  6606  endisj  6790  phplem2  6819  addnnnq0  7390  mulnnnq0  7391  nqprxx  7487  addsrpr  7686  mulsrpr  7687  recidpirq  7799  apreim  8501  mulcanapi  8564  div1  8599  recdivap  8614  divdivap1  8619  divdivap2  8620  divassapi  8664  divdirapi  8665  div23api  8666  div11api  8667  divmuldivapi  8668  divmul13api  8669  divadddivapi  8670  divdivdivapi  8671  lemulge11  8761  negiso  8850  2cnne0  9066  2rene0  9067  1mhlfehlf  9075  halfpm6th  9077  2halves  9086  halfaddsub  9091  avglt1  9095  avglt2  9096  div4p1lem1div2  9110  3halfnz  9288  nneoor  9293  zeo  9296  divlt1lt  9660  divle1le  9661  nnledivrp  9702  fz0to4untppr  10059  2tnp1ge0ge0  10236  frecfzennn  10361  fxnn0nninf  10373  expge1  10492  faclbnd2  10655  4bc2eq6  10687  cjreb  10808  sqrt2gt1lt2  10991  amgm2  11060  xrnegiso  11203  ege2le3  11612  efi4p  11658  efival  11673  cosmul  11686  sin01bnd  11698  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  sincos2sgn  11706  sin4lt0  11707  egt2lt3  11720  3dvdsdec  11802  3dvds2dec  11803  odd2np1  11810  oddge22np1  11818  ltoddhalfle  11830  halfleoddlt  11831  nno  11843  ndvdsi  11870  flodddiv4  11871  flodddiv4lt  11873  flodddiv4t2lthalf  11874  3lcm2e6woprm  12018  6lcm4e12  12019  pcrec  12240  ennnfonelemj0  12334  structfn  12413  ndxslid  12419  strleun  12484  isbasis3g  12684  bl2in  13043  dveflem  13327  cosz12  13341  sinhalfpilem  13352  ptolemy  13385  sincosq1lem  13386  sincosq4sgn  13390  sinq12gt0  13391  cosq23lt0  13394  coseq00topi  13396  coseq0negpitopi  13397  tangtx  13399  sincos4thpi  13401  sincos6thpi  13403  sincos3rdpi  13404  pigt3  13405  coskpi  13409  cos02pilt1  13412  2logb9irrALT  13532  lgsdir2lem1  13569  1lgs  13584  ex-an  13604  ex-fl  13606  ex-exp  13608  bdbm1.3ii  13773  subctctexmid  13881