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  4256  epelg  4437  pwnex  4597  onsucelsucexmid  4679  elvv  4839  relopabiv  4905  funpr  5436  mpov  6181  caovcom  6250  th3q  6918  endisj  7127  phplem2  7159  ssfiexmidt  7185  addnnnq0  7823  mulnnnq0  7824  nqprxx  7920  addsrpr  8119  mulsrpr  8120  recidpirq  8232  apreim  8940  aptap  8987  mulcanapi  9004  div1  9042  recdivap  9057  divdivap1  9062  divdivap2  9063  divassapi  9107  divdirapi  9108  div23api  9109  div11api  9110  divmuldivapi  9111  divmul13api  9112  divadddivapi  9113  divdivdivapi  9114  lemulge11  9205  negiso  9294  2cnne0  9526  2rene0  9527  1mhlfehlf  9535  halfpm6th  9537  2halves  9546  halfaddsub  9551  avglt1  9556  avglt2  9557  div4p1lem1div2  9571  3halfnz  9755  nneoor  9760  zeo  9763  divlt1lt  10143  divle1le  10144  nnledivrp  10185  fz0to4untppr  10549  2tnp1ge0ge0  10758  frecfzennn  10885  xnn0nnen  10896  fxnn0nninf  10898  expge1  11035  faclbnd2  11203  4bc2eq6  11236  cjreb  11654  sqrt2gt1lt2  11838  amgm2  11908  xrnegiso  12054  ege2le3  12464  efi4p  12510  efival  12525  cosmul  12538  sin01bnd  12550  cos01bnd  12551  cos1bnd  12552  cos2bnd  12553  sin01gt0  12555  cos01gt0  12556  sin02gt0  12557  sincos2sgn  12559  sin4lt0  12560  egt2lt3  12573  3dvdsdec  12658  3dvds2dec  12659  odd2np1  12666  oddge22np1  12674  ltoddhalfle  12686  halfleoddlt  12687  nno  12699  ndvdsi  12726  flodddiv4  12729  flodddiv4lt  12731  flodddiv4t2lthalf  12732  bitsp1o  12746  3lcm2e6woprm  12890  6lcm4e12  12891  pcrec  13117  ballotfilemonn  13280  ballotfilemth  13340  ennnfonelemj0  13351  structfn  13430  ndxslid  13436  strleun  13518  slotsdifipndx  13589  slotsdifplendx  13624  slotsdifdsndx  13639  slotsdifunifndx  13646  cnfld1  15019  expghmap  15052  isbasis3g  15284  bl2in  15641  dveflem  15964  cosz12  16019  sinhalfpilem  16030  ptolemy  16063  sincosq1lem  16064  sincosq4sgn  16068  sinq12gt0  16069  cosq23lt0  16072  coseq00topi  16074  coseq0negpitopi  16075  tangtx  16077  sincos4thpi  16079  sincos6thpi  16081  sincos3rdpi  16082  pigt3  16083  coskpi  16087  cos02pilt1  16091  2logb9irrALT  16222  log2tlbndlog2  16232  log2ublem1  16233  log2ublog2  16236  ppiublem1  16303  ppiublem2  16304  ppiqub  16305  chtublem  16307  chtqub  16308  bcmono  16316  bclbnd  16319  bpos1lem  16321  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem4  16326  bposlem5  16327  bposlem6  16328  bposlem7  16329  bposlem8  16330  bposlem9  16331  lgsdir2lem1  16364  1lgs  16379  gausslemma2dlem0c  16387  gausslemma2dlem0d  16388  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  gausslemma2dlem3  16399  lgsquad2lem2  16418  2lgslem1a1  16422  2lgslem1a2  16423  2lgslem1c  16426  2lgslem3  16437  2lgsoddprmlem1  16441  usgrexmpldifpr  16707  uhgrsubgrself  16724  konigsberglem1  16946  ex-an  16954  ex-fl  16956  ex-exp  16958  bdbm1.3ii  17134  subctctexmid  17247  wexmiddifxy  17263  qdiff  17317