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  557  biijust  644  3pm3.2i  1199  sbequilem  1884  unssi  3379  ssini  3427  bm1.3ii  4205  epelg  4382  pwnex  4541  onsucelsucexmid  4623  elvv  4783  relopabiv  4848  funpr  5376  mpov  6103  caovcom  6172  th3q  6800  endisj  6996  phplem2  7027  addnnnq0  7652  mulnnnq0  7653  nqprxx  7749  addsrpr  7948  mulsrpr  7949  recidpirq  8061  apreim  8766  aptap  8813  mulcanapi  8830  div1  8866  recdivap  8881  divdivap1  8886  divdivap2  8887  divassapi  8931  divdirapi  8932  div23api  8933  div11api  8934  divmuldivapi  8935  divmul13api  8936  divadddivapi  8937  divdivdivapi  8938  lemulge11  9029  negiso  9118  2cnne0  9336  2rene0  9337  1mhlfehlf  9345  halfpm6th  9347  2halves  9356  halfaddsub  9361  avglt1  9366  avglt2  9367  div4p1lem1div2  9381  3halfnz  9560  nneoor  9565  zeo  9568  divlt1lt  9937  divle1le  9938  nnledivrp  9979  fz0to4untppr  10337  2tnp1ge0ge0  10538  frecfzennn  10665  xnn0nnen  10676  fxnn0nninf  10678  expge1  10815  faclbnd2  10981  4bc2eq6  11013  cjreb  11398  sqrt2gt1lt2  11581  amgm2  11650  xrnegiso  11794  ege2le3  12203  efi4p  12249  efival  12264  cosmul  12277  sin01bnd  12289  cos01bnd  12290  cos1bnd  12291  cos2bnd  12292  sin01gt0  12294  cos01gt0  12295  sin02gt0  12296  sincos2sgn  12298  sin4lt0  12299  egt2lt3  12312  3dvdsdec  12397  3dvds2dec  12398  odd2np1  12405  oddge22np1  12413  ltoddhalfle  12425  halfleoddlt  12426  nno  12438  ndvdsi  12465  flodddiv4  12468  flodddiv4lt  12470  flodddiv4t2lthalf  12471  bitsp1o  12485  3lcm2e6woprm  12629  6lcm4e12  12630  pcrec  12852  ennnfonelemj0  12993  structfn  13072  ndxslid  13078  strleun  13158  slotsdifipndx  13229  slotsdifplendx  13264  slotsdifdsndx  13279  slotsdifunifndx  13286  cnfld1  14557  expghmap  14592  isbasis3g  14741  bl2in  15098  dveflem  15421  cosz12  15475  sinhalfpilem  15486  ptolemy  15519  sincosq1lem  15520  sincosq4sgn  15524  sinq12gt0  15525  cosq23lt0  15528  coseq00topi  15530  coseq0negpitopi  15531  tangtx  15533  sincos4thpi  15535  sincos6thpi  15537  sincos3rdpi  15538  pigt3  15539  coskpi  15543  cos02pilt1  15546  2logb9irrALT  15669  lgsdir2lem1  15728  1lgs  15743  gausslemma2dlem0c  15751  gausslemma2dlem0d  15752  gausslemma2dlem1a  15758  gausslemma2dlem2  15762  gausslemma2dlem3  15763  lgsquad2lem2  15782  2lgslem1a1  15786  2lgslem1a2  15787  2lgslem1c  15790  2lgslem3  15801  2lgsoddprmlem1  15805  usgrexmpldifpr  16068  ex-an  16196  ex-fl  16198  ex-exp  16200  bdbm1.3ii  16363  subctctexmid  16479