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  3396  ssini  3446  bm1.3ii  4233  epelg  4413  pwnex  4572  onsucelsucexmid  4654  elvv  4814  relopabiv  4880  funpr  5410  mpov  6145  caovcom  6214  th3q  6876  endisj  7077  phplem2  7109  ssfiexmidt  7135  addnnnq0  7769  mulnnnq0  7770  nqprxx  7866  addsrpr  8065  mulsrpr  8066  recidpirq  8178  apreim  8882  aptap  8929  mulcanapi  8946  div1  8982  recdivap  8997  divdivap1  9002  divdivap2  9003  divassapi  9047  divdirapi  9048  div23api  9049  div11api  9050  divmuldivapi  9051  divmul13api  9052  divadddivapi  9053  divdivdivapi  9054  lemulge11  9145  negiso  9234  2cnne0  9452  2rene0  9453  1mhlfehlf  9461  halfpm6th  9463  2halves  9472  halfaddsub  9477  avglt1  9482  avglt2  9483  div4p1lem1div2  9497  3halfnz  9681  nneoor  9686  zeo  9689  divlt1lt  10063  divle1le  10064  nnledivrp  10105  fz0to4untppr  10465  2tnp1ge0ge0  10668  frecfzennn  10795  xnn0nnen  10806  fxnn0nninf  10808  expge1  10945  faclbnd2  11112  4bc2eq6  11145  cjreb  11559  sqrt2gt1lt2  11742  amgm2  11811  xrnegiso  11955  ege2le3  12365  efi4p  12411  efival  12426  cosmul  12439  sin01bnd  12451  cos01bnd  12452  cos1bnd  12453  cos2bnd  12454  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  sincos2sgn  12460  sin4lt0  12461  egt2lt3  12474  3dvdsdec  12559  3dvds2dec  12560  odd2np1  12567  oddge22np1  12575  ltoddhalfle  12587  halfleoddlt  12588  nno  12600  ndvdsi  12627  flodddiv4  12630  flodddiv4lt  12632  flodddiv4t2lthalf  12633  bitsp1o  12647  3lcm2e6woprm  12791  6lcm4e12  12792  pcrec  13014  ballotfilemonn  13148  ennnfonelemj0  13173  structfn  13252  ndxslid  13258  strleun  13338  slotsdifipndx  13409  slotsdifplendx  13444  slotsdifdsndx  13459  slotsdifunifndx  13466  cnfld1  14769  expghmap  14804  isbasis3g  14960  bl2in  15317  dveflem  15640  cosz12  15694  sinhalfpilem  15705  ptolemy  15738  sincosq1lem  15739  sincosq4sgn  15743  sinq12gt0  15744  cosq23lt0  15747  coseq00topi  15749  coseq0negpitopi  15750  tangtx  15752  sincos4thpi  15754  sincos6thpi  15756  sincos3rdpi  15757  pigt3  15758  coskpi  15762  cos02pilt1  15765  2logb9irrALT  15888  lgsdir2lem1  15950  1lgs  15965  gausslemma2dlem0c  15973  gausslemma2dlem0d  15974  gausslemma2dlem1a  15980  gausslemma2dlem2  15984  gausslemma2dlem3  15985  lgsquad2lem2  16004  2lgslem1a1  16008  2lgslem1a2  16009  2lgslem1c  16012  2lgslem3  16023  2lgsoddprmlem1  16027  usgrexmpldifpr  16293  uhgrsubgrself  16310  konigsberglem1  16532  ex-an  16540  ex-fl  16542  ex-exp  16544  bdbm1.3ii  16710  subctctexmid  16823  qdiff  16882