Theorem pm3.2i 257

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

Syntax hints:   ∧ wa 97

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

This theorem is referenced by:  mp4an  403  pm4.87  493  biijust  570  3pm3.2i  1082  sbequilem  1719  unssi  3118  ssini  3160  bm1.3ii  3878  epelg  4027  onsucelsucexmid  4255  elvv  4402  funpr  4951  mpt2v  5594  caovcom  5658  th3q  6211  endisj  6298  phplem2  6316  addnnnq0  6547  mulnnnq0  6548  nqprxx  6644  addsrpr  6830  mulsrpr  6831  recidpirq  6934  apreim  7594  mulcanapi  7648  div1  7680  recdivap  7694  divdivap1  7699  divdivap2  7700  divassapi  7744  divdirapi  7745  div23api  7746  div11api  7747  divmuldivapi  7748  divmul13api  7749  divadddivapi  7750  divdivdivapi  7751  lemulge11  7832  2cnne0  8134  2rene0  8135  1mhlfehlf  8143  halfpm6th  8145  2halves  8154  halfaddsub  8159  avglt1  8163  avglt2  8164  div4p1lem1div2  8177  nneoor  8340  zeo  8343  divlt1lt  8650  divle1le  8651  2tnp1ge0ge0  9143  frecfzennn  9203  expge1  9292  cjreb  9466  sqrt2gt1lt2  9647  amgm2  9714  ex-an  9894  ex-fl  9895  bdbm1.3ii  10011