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  3393  ssini  3443  bm1.3ii  4230  epelg  4410  pwnex  4569  onsucelsucexmid  4651  elvv  4811  relopabiv  4877  funpr  5407  mpov  6142  caovcom  6211  th3q  6873  endisj  7074  phplem2  7106  ssfiexmidt  7132  addnnnq0  7760  mulnnnq0  7761  nqprxx  7857  addsrpr  8056  mulsrpr  8057  recidpirq  8169  apreim  8873  aptap  8920  mulcanapi  8937  div1  8973  recdivap  8988  divdivap1  8993  divdivap2  8994  divassapi  9038  divdirapi  9039  div23api  9040  div11api  9041  divmuldivapi  9042  divmul13api  9043  divadddivapi  9044  divdivdivapi  9045  lemulge11  9136  negiso  9225  2cnne0  9443  2rene0  9444  1mhlfehlf  9452  halfpm6th  9454  2halves  9463  halfaddsub  9468  avglt1  9473  avglt2  9474  div4p1lem1div2  9488  3halfnz  9671  nneoor  9676  zeo  9679  divlt1lt  10053  divle1le  10054  nnledivrp  10095  fz0to4untppr  10454  2tnp1ge0ge0  10657  frecfzennn  10784  xnn0nnen  10795  fxnn0nninf  10797  expge1  10934  faclbnd2  11100  4bc2eq6  11132  cjreb  11544  sqrt2gt1lt2  11727  amgm2  11796  xrnegiso  11940  ege2le3  12350  efi4p  12396  efival  12411  cosmul  12424  sin01bnd  12436  cos01bnd  12437  cos1bnd  12438  cos2bnd  12439  sin01gt0  12441  cos01gt0  12442  sin02gt0  12443  sincos2sgn  12445  sin4lt0  12446  egt2lt3  12459  3dvdsdec  12544  3dvds2dec  12545  odd2np1  12552  oddge22np1  12560  ltoddhalfle  12572  halfleoddlt  12573  nno  12585  ndvdsi  12612  flodddiv4  12615  flodddiv4lt  12617  flodddiv4t2lthalf  12618  bitsp1o  12632  3lcm2e6woprm  12776  6lcm4e12  12777  pcrec  12999  ennnfonelemj0  13141  structfn  13220  ndxslid  13226  strleun  13306  slotsdifipndx  13377  slotsdifplendx  13412  slotsdifdsndx  13427  slotsdifunifndx  13434  cnfld1  14707  expghmap  14742  isbasis3g  14898  bl2in  15255  dveflem  15578  cosz12  15632  sinhalfpilem  15643  ptolemy  15676  sincosq1lem  15677  sincosq4sgn  15681  sinq12gt0  15682  cosq23lt0  15685  coseq00topi  15687  coseq0negpitopi  15688  tangtx  15690  sincos4thpi  15692  sincos6thpi  15694  sincos3rdpi  15695  pigt3  15696  coskpi  15700  cos02pilt1  15703  2logb9irrALT  15826  lgsdir2lem1  15888  1lgs  15903  gausslemma2dlem0c  15911  gausslemma2dlem0d  15912  gausslemma2dlem1a  15918  gausslemma2dlem2  15922  gausslemma2dlem3  15923  lgsquad2lem2  15942  2lgslem1a1  15946  2lgslem1a2  15947  2lgslem1c  15950  2lgslem3  15961  2lgsoddprmlem1  15965  usgrexmpldifpr  16231  uhgrsubgrself  16248  konigsberglem1  16470  ex-an  16478  ex-fl  16480  ex-exp  16482  bdbm1.3ii  16648  subctctexmid  16761  qdiff  16820