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  641  3pm3.2i  1175  sbequilem  1836  unssi  3308  ssini  3356  bm1.3ii  4119  epelg  4284  pwnex  4443  onsucelsucexmid  4523  elvv  4682  funpr  5260  mpov  5955  caovcom  6022  th3q  6630  endisj  6814  phplem2  6843  addnnnq0  7423  mulnnnq0  7424  nqprxx  7520  addsrpr  7719  mulsrpr  7720  recidpirq  7832  apreim  8534  mulcanapi  8597  div1  8632  recdivap  8647  divdivap1  8652  divdivap2  8653  divassapi  8697  divdirapi  8698  div23api  8699  div11api  8700  divmuldivapi  8701  divmul13api  8702  divadddivapi  8703  divdivdivapi  8704  lemulge11  8794  negiso  8883  2cnne0  9099  2rene0  9100  1mhlfehlf  9108  halfpm6th  9110  2halves  9119  halfaddsub  9124  avglt1  9128  avglt2  9129  div4p1lem1div2  9143  3halfnz  9321  nneoor  9326  zeo  9329  divlt1lt  9693  divle1le  9694  nnledivrp  9735  fz0to4untppr  10092  2tnp1ge0ge0  10269  frecfzennn  10394  fxnn0nninf  10406  expge1  10525  faclbnd2  10688  4bc2eq6  10720  cjreb  10841  sqrt2gt1lt2  11024  amgm2  11093  xrnegiso  11236  ege2le3  11645  efi4p  11691  efival  11706  cosmul  11719  sin01bnd  11731  cos01bnd  11732  cos1bnd  11733  cos2bnd  11734  sin01gt0  11735  cos01gt0  11736  sin02gt0  11737  sincos2sgn  11739  sin4lt0  11740  egt2lt3  11753  3dvdsdec  11835  3dvds2dec  11836  odd2np1  11843  oddge22np1  11851  ltoddhalfle  11863  halfleoddlt  11864  nno  11876  ndvdsi  11903  flodddiv4  11904  flodddiv4lt  11906  flodddiv4t2lthalf  11907  3lcm2e6woprm  12051  6lcm4e12  12052  pcrec  12273  ennnfonelemj0  12367  structfn  12446  ndxslid  12452  strleun  12518  slotsdifdsndx  12607  isbasis3g  13095  bl2in  13454  dveflem  13738  cosz12  13752  sinhalfpilem  13763  ptolemy  13796  sincosq1lem  13797  sincosq4sgn  13801  sinq12gt0  13802  cosq23lt0  13805  coseq00topi  13807  coseq0negpitopi  13808  tangtx  13810  sincos4thpi  13812  sincos6thpi  13814  sincos3rdpi  13815  pigt3  13816  coskpi  13820  cos02pilt1  13823  2logb9irrALT  13943  lgsdir2lem1  13980  1lgs  13995  ex-an  14015  ex-fl  14017  ex-exp  14019  bdbm1.3ii  14183  subctctexmid  14291