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  1838  unssi  3310  ssini  3358  bm1.3ii  4122  epelg  4288  pwnex  4447  onsucelsucexmid  4527  elvv  4686  funpr  5265  mpov  5960  caovcom  6027  th3q  6635  endisj  6819  phplem2  6848  addnnnq0  7443  mulnnnq0  7444  nqprxx  7540  addsrpr  7739  mulsrpr  7740  recidpirq  7852  apreim  8554  aptap  8601  mulcanapi  8618  div1  8654  recdivap  8669  divdivap1  8674  divdivap2  8675  divassapi  8719  divdirapi  8720  div23api  8721  div11api  8722  divmuldivapi  8723  divmul13api  8724  divadddivapi  8725  divdivdivapi  8726  lemulge11  8817  negiso  8906  2cnne0  9122  2rene0  9123  1mhlfehlf  9131  halfpm6th  9133  2halves  9142  halfaddsub  9147  avglt1  9151  avglt2  9152  div4p1lem1div2  9166  3halfnz  9344  nneoor  9349  zeo  9352  divlt1lt  9718  divle1le  9719  nnledivrp  9760  fz0to4untppr  10117  2tnp1ge0ge0  10294  frecfzennn  10419  fxnn0nninf  10431  expge1  10550  faclbnd2  10713  4bc2eq6  10745  cjreb  10866  sqrt2gt1lt2  11049  amgm2  11118  xrnegiso  11261  ege2le3  11670  efi4p  11716  efival  11731  cosmul  11744  sin01bnd  11756  cos01bnd  11757  cos1bnd  11758  cos2bnd  11759  sin01gt0  11760  cos01gt0  11761  sin02gt0  11762  sincos2sgn  11764  sin4lt0  11765  egt2lt3  11778  3dvdsdec  11860  3dvds2dec  11861  odd2np1  11868  oddge22np1  11876  ltoddhalfle  11888  halfleoddlt  11889  nno  11901  ndvdsi  11928  flodddiv4  11929  flodddiv4lt  11931  flodddiv4t2lthalf  11932  3lcm2e6woprm  12076  6lcm4e12  12077  pcrec  12298  ennnfonelemj0  12392  structfn  12471  ndxslid  12477  strleun  12553  slotsdifipndx  12623  slotsdifplendx  12655  slotsdifdsndx  12666  slotsdifunifndx  12673  cnfld1  13271  isbasis3g  13326  bl2in  13685  dveflem  13969  cosz12  13983  sinhalfpilem  13994  ptolemy  14027  sincosq1lem  14028  sincosq4sgn  14032  sinq12gt0  14033  cosq23lt0  14036  coseq00topi  14038  coseq0negpitopi  14039  tangtx  14041  sincos4thpi  14043  sincos6thpi  14045  sincos3rdpi  14046  pigt3  14047  coskpi  14051  cos02pilt1  14054  2logb9irrALT  14174  lgsdir2lem1  14211  1lgs  14226  ex-an  14246  ex-fl  14248  ex-exp  14250  bdbm1.3ii  14414  subctctexmid  14521