Theorem mp3an3 1449

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1120	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  mp3an13  1451  mp3an23  1452  mp3anl3  1456  opelxp  5626  ov  7426  ovmpoa  7437  ovmpo  7442  frecseq123  8107  oaword1  8392  oneo  8421  oeoalem  8436  oeoelem  8438  nnaword1  8469  nnneo  8494  erov  8612  enrefg  8781  f1imaen  8811  mapxpen  8939  acnlem  9813  djucomen  9942  nnadju  9962  infmap  10341  canthnumlem  10413  tskin  10524  tsksn  10525  tsk0  10528  gruxp  10572  gruina  10583  genpprecl  10766  addsrpr  10840  mulsrpr  10841  supsrlem  10876  mulid1  10982  00id  11159  mul02lem1  11160  ltneg  11484  leneg  11487  suble0  11498  div1  11673  nnaddcl  12005  nnmulcl  12006  nnge1  12010  nnsub  12026  2halves  12210  halfaddsub  12215  addltmul  12218  frnnn0fsuppg  12301  zleltp1  12380  nnaddm1cl  12386  zextlt  12403  eluzp1p1  12619  uzaddcl  12653  znq  12701  xrre  12912  xrre2  12913  fzshftral  13353  fraclt1  13531  expadd  13834  expmul  13837  sqmul  13848  expubnd  13904  bernneq  13953  faclbnd2  14014  faclbnd6  14022  hashgadd  14101  hashun2  14107  hashunsnggt  14118  hashssdif  14136  hashfun  14161  ccatlcan  14440  ccatrcan  14441  pfx2  14669  shftval3  14796  sqrlem1  14963  caubnd2  15078  bpoly2  15776  bpoly3  15777  fsumcube  15779  efexp  15819  efival  15870  cos01gt0  15909  odd2np1  16059  halfleoddlt  16080  omoe  16082  opeo  16083  divalglem5  16115  gcdmultipleOLD  16269  sqgcd  16279  nn0seqcvgd  16284  prmdvdssq  16432  phiprmpw  16486  eulerthlem2  16492  odzcllem  16502  pythagtriplem15  16539  pythagtriplem17  16541  pcelnn  16580  4sqlem3  16660  fullfunc  17631  fthfunc  17632  prfcl  17929  curf1cl  17955  curfcl  17959  hofcl  17986  odinv  19177  lsmelvalix  19255  dprdval  19615  lsp0  20280  lss0v  20287  zndvds0  20767  frlmlbs  21013  lindfres  21039  lmisfree  21058  coe1scl  21467  ntrin  22221  lpsscls  22301  restperf  22344  txuni2  22725  txopn  22762  elqtop2  22861  xkocnv  22974  ptcmp  23218  xblpnfps  23557  xblpnf  23558  bl2in  23562  unirnblps  23581  unirnbl  23582  blpnfctr  23598  dscopn  23738  bcthlem4  24500  minveclem2  24599  minveclem4  24605  icombl  24737  i1fadd  24868  i1fmul  24869  dvn1  25099  dvexp3  25151  plyconst  25376  plyid  25379  sincosq1eq  25678  sinord  25699  cxpp1  25844  cxpsqrtlem  25866  cxpsqrt  25867  angneg  25962  dcubic  26005  issqf  26294  ppiub  26361  bposlem1  26441  bposlem2  26442  bposlem9  26449  axlowdimlem6  27324  axlowdimlem14  27332  axcontlem2  27342  pthdlem2  28145  0ewlk  28487  ipasslem1  29202  ipasslem2  29203  ipasslem11  29211  minvecolem2  29246  minvecolem3  29247  minvecolem4  29251  shsva  29691  h1datomi  29952  lnfnmuli  30415  leopsq  30500  nmopleid  30510  opsqrlem6  30516  pjnmopi  30519  hstle  30601  csmdsymi  30705  atcvatlem  30756  dpfrac1  31175  cshf1o  31243  cycpmconjslem2  31431  rspidlid  31579  elsx  32171  dya2iocnrect  32257  cvmliftphtlem  33288  satfv1  33334  satffunlem1lem2  33374  satffunlem1  33378  wlimeq12  33822  nosupno  33915  nosupfv  33918  noinfno  33930  noinffv  33933  scutval  34003  scutun12  34013  cofcut1  34099  cofcutr  34101  fvray  34452  fvline  34455  tailfb  34575  uncov  35767  tan2h  35778  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem32  35818  mblfinlem4  35826  mbfresfi  35832  mbfposadd  35833  itg2addnc  35840  ftc1anclem5  35863  ftc1anclem8  35866  dvasin  35870  heiborlem7  35984  igenidl  36230  el3v3  36383  atlatmstc  37340  dihglblem2N  39315  2xp3dxp2ge1d  40169  factwoffsmonot  40170  eldioph4b  40640  diophren  40642  rmxp1  40761  rmyp1  40762  rmxm1  40763  rmym1  40764  dig0  45963  i0oii  46224  onetansqsecsq  46474  cotsqcscsq  46475