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  1180  sbequilem  1864  unssi  3359  ssini  3407  bm1.3ii  4184  epelg  4358  pwnex  4517  onsucelsucexmid  4599  elvv  4758  relopabiv  4822  funpr  5349  mpov  6065  caovcom  6134  th3q  6757  endisj  6951  phplem2  6982  addnnnq0  7604  mulnnnq0  7605  nqprxx  7701  addsrpr  7900  mulsrpr  7901  recidpirq  8013  apreim  8718  aptap  8765  mulcanapi  8782  div1  8818  recdivap  8833  divdivap1  8838  divdivap2  8839  divassapi  8883  divdirapi  8884  div23api  8885  div11api  8886  divmuldivapi  8887  divmul13api  8888  divadddivapi  8889  divdivdivapi  8890  lemulge11  8981  negiso  9070  2cnne0  9288  2rene0  9289  1mhlfehlf  9297  halfpm6th  9299  2halves  9308  halfaddsub  9313  avglt1  9318  avglt2  9319  div4p1lem1div2  9333  3halfnz  9512  nneoor  9517  zeo  9520  divlt1lt  9888  divle1le  9889  nnledivrp  9930  fz0to4untppr  10288  2tnp1ge0ge0  10488  frecfzennn  10615  xnn0nnen  10626  fxnn0nninf  10628  expge1  10765  faclbnd2  10931  4bc2eq6  10963  cjreb  11343  sqrt2gt1lt2  11526  amgm2  11595  xrnegiso  11739  ege2le3  12148  efi4p  12194  efival  12209  cosmul  12222  sin01bnd  12234  cos01bnd  12235  cos1bnd  12236  cos2bnd  12237  sin01gt0  12239  cos01gt0  12240  sin02gt0  12241  sincos2sgn  12243  sin4lt0  12244  egt2lt3  12257  3dvdsdec  12342  3dvds2dec  12343  odd2np1  12350  oddge22np1  12358  ltoddhalfle  12370  halfleoddlt  12371  nno  12383  ndvdsi  12410  flodddiv4  12413  flodddiv4lt  12415  flodddiv4t2lthalf  12416  bitsp1o  12430  3lcm2e6woprm  12574  6lcm4e12  12575  pcrec  12797  ennnfonelemj0  12938  structfn  13017  ndxslid  13023  strleun  13103  slotsdifipndx  13174  slotsdifplendx  13209  slotsdifdsndx  13224  slotsdifunifndx  13231  cnfld1  14501  expghmap  14536  isbasis3g  14685  bl2in  15042  dveflem  15365  cosz12  15419  sinhalfpilem  15430  ptolemy  15463  sincosq1lem  15464  sincosq4sgn  15468  sinq12gt0  15469  cosq23lt0  15472  coseq00topi  15474  coseq0negpitopi  15475  tangtx  15477  sincos4thpi  15479  sincos6thpi  15481  sincos3rdpi  15482  pigt3  15483  coskpi  15487  cos02pilt1  15490  2logb9irrALT  15613  lgsdir2lem1  15672  1lgs  15687  gausslemma2dlem0c  15695  gausslemma2dlem0d  15696  gausslemma2dlem1a  15702  gausslemma2dlem2  15706  gausslemma2dlem3  15707  lgsquad2lem2  15726  2lgslem1a1  15730  2lgslem1a2  15731  2lgslem1c  15734  2lgslem3  15745  2lgsoddprmlem1  15749  ex-an  15997  ex-fl  15999  ex-exp  16001  bdbm1.3ii  16164  subctctexmid  16277