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  644  3pm3.2i  1199  sbequilem  1884  unssi  3379  ssini  3427  bm1.3ii  4205  epelg  4381  pwnex  4540  onsucelsucexmid  4622  elvv  4781  relopabiv  4845  funpr  5373  mpov  6100  caovcom  6169  th3q  6795  endisj  6991  phplem2  7022  addnnnq0  7644  mulnnnq0  7645  nqprxx  7741  addsrpr  7940  mulsrpr  7941  recidpirq  8053  apreim  8758  aptap  8805  mulcanapi  8822  div1  8858  recdivap  8873  divdivap1  8878  divdivap2  8879  divassapi  8923  divdirapi  8924  div23api  8925  div11api  8926  divmuldivapi  8927  divmul13api  8928  divadddivapi  8929  divdivdivapi  8930  lemulge11  9021  negiso  9110  2cnne0  9328  2rene0  9329  1mhlfehlf  9337  halfpm6th  9339  2halves  9348  halfaddsub  9353  avglt1  9358  avglt2  9359  div4p1lem1div2  9373  3halfnz  9552  nneoor  9557  zeo  9560  divlt1lt  9928  divle1le  9929  nnledivrp  9970  fz0to4untppr  10328  2tnp1ge0ge0  10529  frecfzennn  10656  xnn0nnen  10667  fxnn0nninf  10669  expge1  10806  faclbnd2  10972  4bc2eq6  11004  cjreb  11385  sqrt2gt1lt2  11568  amgm2  11637  xrnegiso  11781  ege2le3  12190  efi4p  12236  efival  12251  cosmul  12264  sin01bnd  12276  cos01bnd  12277  cos1bnd  12278  cos2bnd  12279  sin01gt0  12281  cos01gt0  12282  sin02gt0  12283  sincos2sgn  12285  sin4lt0  12286  egt2lt3  12299  3dvdsdec  12384  3dvds2dec  12385  odd2np1  12392  oddge22np1  12400  ltoddhalfle  12412  halfleoddlt  12413  nno  12425  ndvdsi  12452  flodddiv4  12455  flodddiv4lt  12457  flodddiv4t2lthalf  12458  bitsp1o  12472  3lcm2e6woprm  12616  6lcm4e12  12617  pcrec  12839  ennnfonelemj0  12980  structfn  13059  ndxslid  13065  strleun  13145  slotsdifipndx  13216  slotsdifplendx  13251  slotsdifdsndx  13266  slotsdifunifndx  13273  cnfld1  14544  expghmap  14579  isbasis3g  14728  bl2in  15085  dveflem  15408  cosz12  15462  sinhalfpilem  15473  ptolemy  15506  sincosq1lem  15507  sincosq4sgn  15511  sinq12gt0  15512  cosq23lt0  15515  coseq00topi  15517  coseq0negpitopi  15518  tangtx  15520  sincos4thpi  15522  sincos6thpi  15524  sincos3rdpi  15525  pigt3  15526  coskpi  15530  cos02pilt1  15533  2logb9irrALT  15656  lgsdir2lem1  15715  1lgs  15730  gausslemma2dlem0c  15738  gausslemma2dlem0d  15739  gausslemma2dlem1a  15745  gausslemma2dlem2  15749  gausslemma2dlem3  15750  lgsquad2lem2  15769  2lgslem1a1  15773  2lgslem1a2  15774  2lgslem1c  15777  2lgslem3  15788  2lgsoddprmlem1  15792  ex-an  16111  ex-fl  16113  ex-exp  16115  bdbm1.3ii  16278  subctctexmid  16395