Theorem pm3.2i 270

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-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  mp4an  423  pm4.87  546  biijust  630  3pm3.2i  1159  sbequilem  1810  unssi  3246  ssini  3294  bm1.3ii  4044  epelg  4207  pwnex  4365  onsucelsucexmid  4440  elvv  4596  funpr  5170  mpov  5854  caovcom  5921  th3q  6527  endisj  6711  phplem2  6740  addnnnq0  7250  mulnnnq0  7251  nqprxx  7347  addsrpr  7546  mulsrpr  7547  recidpirq  7659  apreim  8358  mulcanapi  8421  div1  8456  recdivap  8471  divdivap1  8476  divdivap2  8477  divassapi  8521  divdirapi  8522  div23api  8523  div11api  8524  divmuldivapi  8525  divmul13api  8526  divadddivapi  8527  divdivdivapi  8528  lemulge11  8617  negiso  8706  2cnne0  8922  2rene0  8923  1mhlfehlf  8931  halfpm6th  8933  2halves  8942  halfaddsub  8947  avglt1  8951  avglt2  8952  div4p1lem1div2  8966  3halfnz  9141  nneoor  9146  zeo  9149  divlt1lt  9504  divle1le  9505  nnledivrp  9546  2tnp1ge0ge0  10067  frecfzennn  10192  fxnn0nninf  10204  expge1  10323  faclbnd2  10481  4bc2eq6  10513  cjreb  10631  sqrt2gt1lt2  10814  amgm2  10883  xrnegiso  11024  ege2le3  11366  efi4p  11413  efival  11428  cosmul  11441  sin01bnd  11453  cos01bnd  11454  cos1bnd  11455  cos2bnd  11456  sin01gt0  11457  cos01gt0  11458  sin02gt0  11459  sincos2sgn  11461  sin4lt0  11462  egt2lt3  11475  3dvdsdec  11551  3dvds2dec  11552  odd2np1  11559  oddge22np1  11567  ltoddhalfle  11579  halfleoddlt  11580  nno  11592  ndvdsi  11619  flodddiv4  11620  flodddiv4lt  11622  flodddiv4t2lthalf  11623  3lcm2e6woprm  11756  6lcm4e12  11757  ennnfonelemj0  11903  structfn  11967  ndxslid  11973  strleun  12037  isbasis3g  12202  bl2in  12561  dveflem  12844  cosz12  12850  sinhalfpilem  12861  ptolemy  12894  sincosq1lem  12895  sincosq4sgn  12899  sinq12gt0  12900  cosq23lt0  12903  coseq00topi  12905  coseq0negpitopi  12906  tangtx  12908  sincos4thpi  12910  sincos6thpi  12912  sincos3rdpi  12913  pigt3  12914  coskpi  12918  cos02pilt1  12921  ex-an  12924  ex-fl  12926  ex-exp  12928  bdbm1.3ii  13078  subctctexmid  13185