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  1852  unssi  3339  ssini  3387  bm1.3ii  4155  epelg  4326  pwnex  4485  onsucelsucexmid  4567  elvv  4726  relopabiv  4790  funpr  5311  mpov  6016  caovcom  6085  th3q  6708  endisj  6892  phplem2  6923  addnnnq0  7535  mulnnnq0  7536  nqprxx  7632  addsrpr  7831  mulsrpr  7832  recidpirq  7944  apreim  8649  aptap  8696  mulcanapi  8713  div1  8749  recdivap  8764  divdivap1  8769  divdivap2  8770  divassapi  8814  divdirapi  8815  div23api  8816  div11api  8817  divmuldivapi  8818  divmul13api  8819  divadddivapi  8820  divdivdivapi  8821  lemulge11  8912  negiso  9001  2cnne0  9219  2rene0  9220  1mhlfehlf  9228  halfpm6th  9230  2halves  9239  halfaddsub  9244  avglt1  9249  avglt2  9250  div4p1lem1div2  9264  3halfnz  9442  nneoor  9447  zeo  9450  divlt1lt  9818  divle1le  9819  nnledivrp  9860  fz0to4untppr  10218  2tnp1ge0ge0  10410  frecfzennn  10537  xnn0nnen  10548  fxnn0nninf  10550  expge1  10687  faclbnd2  10853  4bc2eq6  10885  cjreb  11050  sqrt2gt1lt2  11233  amgm2  11302  xrnegiso  11446  ege2le3  11855  efi4p  11901  efival  11916  cosmul  11929  sin01bnd  11941  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  sincos2sgn  11950  sin4lt0  11951  egt2lt3  11964  3dvdsdec  12049  3dvds2dec  12050  odd2np1  12057  oddge22np1  12065  ltoddhalfle  12077  halfleoddlt  12078  nno  12090  ndvdsi  12117  flodddiv4  12120  flodddiv4lt  12122  flodddiv4t2lthalf  12123  bitsp1o  12137  3lcm2e6woprm  12281  6lcm4e12  12282  pcrec  12504  ennnfonelemj0  12645  structfn  12724  ndxslid  12730  strleun  12809  slotsdifipndx  12879  slotsdifplendx  12914  slotsdifdsndx  12929  slotsdifunifndx  12936  cnfld1  14206  expghmap  14241  isbasis3g  14368  bl2in  14725  dveflem  15048  cosz12  15102  sinhalfpilem  15113  ptolemy  15146  sincosq1lem  15147  sincosq4sgn  15151  sinq12gt0  15152  cosq23lt0  15155  coseq00topi  15157  coseq0negpitopi  15158  tangtx  15160  sincos4thpi  15162  sincos6thpi  15164  sincos3rdpi  15165  pigt3  15166  coskpi  15170  cos02pilt1  15173  2logb9irrALT  15296  lgsdir2lem1  15355  1lgs  15370  gausslemma2dlem0c  15378  gausslemma2dlem0d  15379  gausslemma2dlem1a  15385  gausslemma2dlem2  15389  gausslemma2dlem3  15390  lgsquad2lem2  15409  2lgslem1a1  15413  2lgslem1a2  15414  2lgslem1c  15417  2lgslem3  15428  2lgsoddprmlem1  15432  ex-an  15455  ex-fl  15457  ex-exp  15459  bdbm1.3ii  15623  subctctexmid  15733