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  3380  ssini  3428  bm1.3ii  4208  epelg  4385  pwnex  4544  onsucelsucexmid  4626  elvv  4786  relopabiv  4851  funpr  5379  mpov  6106  caovcom  6175  th3q  6804  endisj  7003  phplem2  7034  ssfiexmidt  7060  addnnnq0  7662  mulnnnq0  7663  nqprxx  7759  addsrpr  7958  mulsrpr  7959  recidpirq  8071  apreim  8776  aptap  8823  mulcanapi  8840  div1  8876  recdivap  8891  divdivap1  8896  divdivap2  8897  divassapi  8941  divdirapi  8942  div23api  8943  div11api  8944  divmuldivapi  8945  divmul13api  8946  divadddivapi  8947  divdivdivapi  8948  lemulge11  9039  negiso  9128  2cnne0  9346  2rene0  9347  1mhlfehlf  9355  halfpm6th  9357  2halves  9366  halfaddsub  9371  avglt1  9376  avglt2  9377  div4p1lem1div2  9391  3halfnz  9570  nneoor  9575  zeo  9578  divlt1lt  9952  divle1le  9953  nnledivrp  9994  fz0to4untppr  10352  2tnp1ge0ge0  10554  frecfzennn  10681  xnn0nnen  10692  fxnn0nninf  10694  expge1  10831  faclbnd2  10997  4bc2eq6  11029  cjreb  11420  sqrt2gt1lt2  11603  amgm2  11672  xrnegiso  11816  ege2le3  12225  efi4p  12271  efival  12286  cosmul  12299  sin01bnd  12311  cos01bnd  12312  cos1bnd  12313  cos2bnd  12314  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  sincos2sgn  12320  sin4lt0  12321  egt2lt3  12334  3dvdsdec  12419  3dvds2dec  12420  odd2np1  12427  oddge22np1  12435  ltoddhalfle  12447  halfleoddlt  12448  nno  12460  ndvdsi  12487  flodddiv4  12490  flodddiv4lt  12492  flodddiv4t2lthalf  12493  bitsp1o  12507  3lcm2e6woprm  12651  6lcm4e12  12652  pcrec  12874  ennnfonelemj0  13015  structfn  13094  ndxslid  13100  strleun  13180  slotsdifipndx  13251  slotsdifplendx  13286  slotsdifdsndx  13301  slotsdifunifndx  13308  cnfld1  14579  expghmap  14614  isbasis3g  14763  bl2in  15120  dveflem  15443  cosz12  15497  sinhalfpilem  15508  ptolemy  15541  sincosq1lem  15542  sincosq4sgn  15546  sinq12gt0  15547  cosq23lt0  15550  coseq00topi  15552  coseq0negpitopi  15553  tangtx  15555  sincos4thpi  15557  sincos6thpi  15559  sincos3rdpi  15560  pigt3  15561  coskpi  15565  cos02pilt1  15568  2logb9irrALT  15691  lgsdir2lem1  15750  1lgs  15765  gausslemma2dlem0c  15773  gausslemma2dlem0d  15774  gausslemma2dlem1a  15780  gausslemma2dlem2  15784  gausslemma2dlem3  15785  lgsquad2lem2  15804  2lgslem1a1  15808  2lgslem1a2  15809  2lgslem1c  15812  2lgslem3  15823  2lgsoddprmlem1  15827  usgrexmpldifpr  16093  ex-an  16269  ex-fl  16271  ex-exp  16273  bdbm1.3ii  16436  subctctexmid  16551