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  1178  sbequilem  1862  unssi  3349  ssini  3397  bm1.3ii  4169  epelg  4341  pwnex  4500  onsucelsucexmid  4582  elvv  4741  relopabiv  4805  funpr  5331  mpov  6042  caovcom  6111  th3q  6734  endisj  6926  phplem2  6957  addnnnq0  7569  mulnnnq0  7570  nqprxx  7666  addsrpr  7865  mulsrpr  7866  recidpirq  7978  apreim  8683  aptap  8730  mulcanapi  8747  div1  8783  recdivap  8798  divdivap1  8803  divdivap2  8804  divassapi  8848  divdirapi  8849  div23api  8850  div11api  8851  divmuldivapi  8852  divmul13api  8853  divadddivapi  8854  divdivdivapi  8855  lemulge11  8946  negiso  9035  2cnne0  9253  2rene0  9254  1mhlfehlf  9262  halfpm6th  9264  2halves  9273  halfaddsub  9278  avglt1  9283  avglt2  9284  div4p1lem1div2  9298  3halfnz  9477  nneoor  9482  zeo  9485  divlt1lt  9853  divle1le  9854  nnledivrp  9895  fz0to4untppr  10253  2tnp1ge0ge0  10451  frecfzennn  10578  xnn0nnen  10589  fxnn0nninf  10591  expge1  10728  faclbnd2  10894  4bc2eq6  10926  cjreb  11221  sqrt2gt1lt2  11404  amgm2  11473  xrnegiso  11617  ege2le3  12026  efi4p  12072  efival  12087  cosmul  12100  sin01bnd  12112  cos01bnd  12113  cos1bnd  12114  cos2bnd  12115  sin01gt0  12117  cos01gt0  12118  sin02gt0  12119  sincos2sgn  12121  sin4lt0  12122  egt2lt3  12135  3dvdsdec  12220  3dvds2dec  12221  odd2np1  12228  oddge22np1  12236  ltoddhalfle  12248  halfleoddlt  12249  nno  12261  ndvdsi  12288  flodddiv4  12291  flodddiv4lt  12293  flodddiv4t2lthalf  12294  bitsp1o  12308  3lcm2e6woprm  12452  6lcm4e12  12453  pcrec  12675  ennnfonelemj0  12816  structfn  12895  ndxslid  12901  strleun  12980  slotsdifipndx  13051  slotsdifplendx  13086  slotsdifdsndx  13101  slotsdifunifndx  13108  cnfld1  14378  expghmap  14413  isbasis3g  14562  bl2in  14919  dveflem  15242  cosz12  15296  sinhalfpilem  15307  ptolemy  15340  sincosq1lem  15341  sincosq4sgn  15345  sinq12gt0  15346  cosq23lt0  15349  coseq00topi  15351  coseq0negpitopi  15352  tangtx  15354  sincos4thpi  15356  sincos6thpi  15358  sincos3rdpi  15359  pigt3  15360  coskpi  15364  cos02pilt1  15367  2logb9irrALT  15490  lgsdir2lem1  15549  1lgs  15564  gausslemma2dlem0c  15572  gausslemma2dlem0d  15573  gausslemma2dlem1a  15579  gausslemma2dlem2  15583  gausslemma2dlem3  15584  lgsquad2lem2  15603  2lgslem1a1  15607  2lgslem1a2  15608  2lgslem1c  15611  2lgslem3  15622  2lgsoddprmlem1  15626  ex-an  15733  ex-fl  15735  ex-exp  15737  bdbm1.3ii  15901  subctctexmid  16011