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  1201  sbequilem  1885  unssi  3381  ssini  3429  bm1.3ii  4211  epelg  4389  pwnex  4548  onsucelsucexmid  4630  elvv  4790  relopabiv  4855  funpr  5384  mpov  6116  caovcom  6185  th3q  6814  endisj  7013  phplem2  7044  ssfiexmidt  7070  addnnnq0  7674  mulnnnq0  7675  nqprxx  7771  addsrpr  7970  mulsrpr  7971  recidpirq  8083  apreim  8788  aptap  8835  mulcanapi  8852  div1  8888  recdivap  8903  divdivap1  8908  divdivap2  8909  divassapi  8953  divdirapi  8954  div23api  8955  div11api  8956  divmuldivapi  8957  divmul13api  8958  divadddivapi  8959  divdivdivapi  8960  lemulge11  9051  negiso  9140  2cnne0  9358  2rene0  9359  1mhlfehlf  9367  halfpm6th  9369  2halves  9378  halfaddsub  9383  avglt1  9388  avglt2  9389  div4p1lem1div2  9403  3halfnz  9582  nneoor  9587  zeo  9590  divlt1lt  9964  divle1le  9965  nnledivrp  10006  fz0to4untppr  10364  2tnp1ge0ge0  10567  frecfzennn  10694  xnn0nnen  10705  fxnn0nninf  10707  expge1  10844  faclbnd2  11010  4bc2eq6  11042  cjreb  11449  sqrt2gt1lt2  11632  amgm2  11701  xrnegiso  11845  ege2le3  12255  efi4p  12301  efival  12316  cosmul  12329  sin01bnd  12341  cos01bnd  12342  cos1bnd  12343  cos2bnd  12344  sin01gt0  12346  cos01gt0  12347  sin02gt0  12348  sincos2sgn  12350  sin4lt0  12351  egt2lt3  12364  3dvdsdec  12449  3dvds2dec  12450  odd2np1  12457  oddge22np1  12465  ltoddhalfle  12477  halfleoddlt  12478  nno  12490  ndvdsi  12517  flodddiv4  12520  flodddiv4lt  12522  flodddiv4t2lthalf  12523  bitsp1o  12537  3lcm2e6woprm  12681  6lcm4e12  12682  pcrec  12904  ennnfonelemj0  13045  structfn  13124  ndxslid  13130  strleun  13210  slotsdifipndx  13281  slotsdifplendx  13316  slotsdifdsndx  13331  slotsdifunifndx  13338  cnfld1  14610  expghmap  14645  isbasis3g  14799  bl2in  15156  dveflem  15479  cosz12  15533  sinhalfpilem  15544  ptolemy  15577  sincosq1lem  15578  sincosq4sgn  15582  sinq12gt0  15583  cosq23lt0  15586  coseq00topi  15588  coseq0negpitopi  15589  tangtx  15591  sincos4thpi  15593  sincos6thpi  15595  sincos3rdpi  15596  pigt3  15597  coskpi  15601  cos02pilt1  15604  2logb9irrALT  15727  lgsdir2lem1  15786  1lgs  15801  gausslemma2dlem0c  15809  gausslemma2dlem0d  15810  gausslemma2dlem1a  15816  gausslemma2dlem2  15820  gausslemma2dlem3  15821  lgsquad2lem2  15840  2lgslem1a1  15844  2lgslem1a2  15845  2lgslem1c  15848  2lgslem3  15859  2lgsoddprmlem1  15863  usgrexmpldifpr  16129  uhgrsubgrself  16146  konigsberglem1  16368  ex-an  16376  ex-fl  16378  ex-exp  16380  bdbm1.3ii  16546  subctctexmid  16661  qdiff  16720