Theorem pm3.2i 268

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 138	. 2 ⊢ (𝜑 → (𝜓 → (𝜑 ∧ 𝜓)))
4	1, 2, 3	mp2 16	1 ⊢ (𝜑 ∧ 𝜓)

Syntax hints:   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  mp4an  421  pm4.87  527  biijust  610  3pm3.2i  1127  sbequilem  1777  unssi  3198  ssini  3246  bm1.3ii  3989  epelg  4150  pwnex  4308  onsucelsucexmid  4383  elvv  4539  funpr  5111  mpov  5793  caovcom  5860  th3q  6464  endisj  6647  phplem2  6676  addnnnq0  7158  mulnnnq0  7159  nqprxx  7255  addsrpr  7441  mulsrpr  7442  recidpirq  7545  apreim  8231  mulcanapi  8289  div1  8324  recdivap  8339  divdivap1  8344  divdivap2  8345  divassapi  8389  divdirapi  8390  div23api  8391  div11api  8392  divmuldivapi  8393  divmul13api  8394  divadddivapi  8395  divdivdivapi  8396  lemulge11  8482  negiso  8571  2cnne0  8781  2rene0  8782  1mhlfehlf  8790  halfpm6th  8792  2halves  8801  halfaddsub  8806  avglt1  8810  avglt2  8811  div4p1lem1div2  8825  3halfnz  9000  nneoor  9005  zeo  9008  divlt1lt  9358  divle1le  9359  nnledivrp  9394  2tnp1ge0ge0  9915  frecfzennn  10040  fxnn0nninf  10052  expge1  10171  faclbnd2  10329  4bc2eq6  10361  cjreb  10479  sqrt2gt1lt2  10661  amgm2  10730  xrnegiso  10870  ege2le3  11175  efi4p  11222  efival  11237  cosmul  11250  sin01bnd  11262  cos01bnd  11263  cos1bnd  11264  cos2bnd  11265  sin01gt0  11266  cos01gt0  11267  sin02gt0  11268  sincos2sgn  11270  sin4lt0  11271  egt2lt3  11281  3dvdsdec  11357  3dvds2dec  11358  odd2np1  11365  oddge22np1  11373  ltoddhalfle  11385  halfleoddlt  11386  nno  11398  ndvdsi  11425  flodddiv4  11426  flodddiv4lt  11428  flodddiv4t2lthalf  11429  3lcm2e6woprm  11560  6lcm4e12  11561  ennnfonelemj0  11706  structfn  11760  ndxslid  11766  strleun  11830  isbasis3g  11995  bl2in  12331  ex-an  12538  ex-fl  12540  ex-exp  12542  bdbm1.3ii  12670