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  642  3pm3.2i  1177  sbequilem  1849  unssi  3335  ssini  3383  bm1.3ii  4151  epelg  4322  pwnex  4481  onsucelsucexmid  4563  elvv  4722  relopabiv  4786  funpr  5307  mpov  6009  caovcom  6078  th3q  6696  endisj  6880  phplem2  6911  addnnnq0  7511  mulnnnq0  7512  nqprxx  7608  addsrpr  7807  mulsrpr  7808  recidpirq  7920  apreim  8624  aptap  8671  mulcanapi  8688  div1  8724  recdivap  8739  divdivap1  8744  divdivap2  8745  divassapi  8789  divdirapi  8790  div23api  8791  div11api  8792  divmuldivapi  8793  divmul13api  8794  divadddivapi  8795  divdivdivapi  8796  lemulge11  8887  negiso  8976  2cnne0  9194  2rene0  9195  1mhlfehlf  9203  halfpm6th  9205  2halves  9214  halfaddsub  9219  avglt1  9224  avglt2  9225  div4p1lem1div2  9239  3halfnz  9417  nneoor  9422  zeo  9425  divlt1lt  9793  divle1le  9794  nnledivrp  9835  fz0to4untppr  10193  2tnp1ge0ge0  10373  frecfzennn  10500  xnn0nnen  10511  fxnn0nninf  10513  expge1  10650  faclbnd2  10816  4bc2eq6  10848  cjreb  11013  sqrt2gt1lt2  11196  amgm2  11265  xrnegiso  11408  ege2le3  11817  efi4p  11863  efival  11878  cosmul  11891  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  sincos2sgn  11912  sin4lt0  11913  egt2lt3  11926  3dvdsdec  12009  3dvds2dec  12010  odd2np1  12017  oddge22np1  12025  ltoddhalfle  12037  halfleoddlt  12038  nno  12050  ndvdsi  12077  flodddiv4  12078  flodddiv4lt  12080  flodddiv4t2lthalf  12081  3lcm2e6woprm  12227  6lcm4e12  12228  pcrec  12449  ennnfonelemj0  12561  structfn  12640  ndxslid  12646  strleun  12725  slotsdifipndx  12795  slotsdifplendx  12830  slotsdifdsndx  12841  slotsdifunifndx  12848  cnfld1  14071  expghmap  14106  isbasis3g  14225  bl2in  14582  dveflem  14905  cosz12  14956  sinhalfpilem  14967  ptolemy  15000  sincosq1lem  15001  sincosq4sgn  15005  sinq12gt0  15006  cosq23lt0  15009  coseq00topi  15011  coseq0negpitopi  15012  tangtx  15014  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  coskpi  15024  cos02pilt1  15027  2logb9irrALT  15147  lgsdir2lem1  15185  1lgs  15200  gausslemma2dlem0c  15208  gausslemma2dlem0d  15209  gausslemma2dlem1a  15215  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquad2lem2  15239  2lgslem1a1  15243  2lgslem1a2  15244  2lgslem1c  15247  2lgslem3  15258  2lgsoddprmlem1  15262  ex-an  15285  ex-fl  15287  ex-exp  15289  bdbm1.3ii  15453  subctctexmid  15561