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  431  pm4.87  563  biijust  650  3pm3.2i  1206  sbequilem  1891  unssi  3404  ssini  3454  bm1.3ii  4252  epelg  4433  pwnex  4593  onsucelsucexmid  4675  elvv  4835  relopabiv  4901  funpr  5431  mpov  6172  caovcom  6241  th3q  6908  endisj  7116  phplem2  7148  ssfiexmidt  7174  addnnnq0  7810  mulnnnq0  7811  nqprxx  7907  addsrpr  8106  mulsrpr  8107  recidpirq  8219  apreim  8925  aptap  8972  mulcanapi  8989  div1  9027  recdivap  9042  divdivap1  9047  divdivap2  9048  divassapi  9092  divdirapi  9093  div23api  9094  div11api  9095  divmuldivapi  9096  divmul13api  9097  divadddivapi  9098  divdivdivapi  9099  lemulge11  9190  negiso  9279  2cnne0  9497  2rene0  9498  1mhlfehlf  9506  halfpm6th  9508  2halves  9517  halfaddsub  9522  avglt1  9527  avglt2  9528  div4p1lem1div2  9542  3halfnz  9726  nneoor  9731  zeo  9734  divlt1lt  10108  divle1le  10109  nnledivrp  10150  fz0to4untppr  10514  2tnp1ge0ge0  10719  frecfzennn  10846  xnn0nnen  10857  fxnn0nninf  10859  expge1  10996  faclbnd2  11163  4bc2eq6  11196  cjreb  11614  sqrt2gt1lt2  11798  amgm2  11867  xrnegiso  12011  ege2le3  12421  efi4p  12467  efival  12482  cosmul  12495  sin01bnd  12507  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  sincos2sgn  12516  sin4lt0  12517  egt2lt3  12530  3dvdsdec  12615  3dvds2dec  12616  odd2np1  12623  oddge22np1  12631  ltoddhalfle  12643  halfleoddlt  12644  nno  12656  ndvdsi  12683  flodddiv4  12686  flodddiv4lt  12688  flodddiv4t2lthalf  12689  bitsp1o  12703  3lcm2e6woprm  12847  6lcm4e12  12848  pcrec  13070  ballotfilemonn  13204  ballotfilemth  13264  ennnfonelemj0  13275  structfn  13354  ndxslid  13360  strleun  13441  slotsdifipndx  13512  slotsdifplendx  13547  slotsdifdsndx  13562  slotsdifunifndx  13569  cnfld1  14892  expghmap  14925  isbasis3g  15130  bl2in  15487  dveflem  15810  cosz12  15864  sinhalfpilem  15875  ptolemy  15908  sincosq1lem  15909  sincosq4sgn  15913  sinq12gt0  15914  cosq23lt0  15917  coseq00topi  15919  coseq0negpitopi  15920  tangtx  15922  sincos4thpi  15924  sincos6thpi  15926  sincos3rdpi  15927  pigt3  15928  coskpi  15932  cos02pilt1  15935  2logb9irrALT  16059  log2tlbndlog2  16065  log2ublem1  16066  log2ublog2  16069  lgsdir2lem1  16130  1lgs  16145  gausslemma2dlem0c  16153  gausslemma2dlem0d  16154  gausslemma2dlem1a  16160  gausslemma2dlem2  16164  gausslemma2dlem3  16165  lgsquad2lem2  16184  2lgslem1a1  16188  2lgslem1a2  16189  2lgslem1c  16192  2lgslem3  16203  2lgsoddprmlem1  16207  usgrexmpldifpr  16473  uhgrsubgrself  16490  konigsberglem1  16712  ex-an  16720  ex-fl  16722  ex-exp  16724  bdbm1.3ii  16900  subctctexmid  17013  qdiff  17072