Theorem mp3an3 1453

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 1122	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mp3an13  1455  mp3an23  1456  mp3anl3  1460  el3v3  3448  opelxp  5659  ov  7502  ovmpoa  7513  ovmpo  7518  frecseq123  8224  oaword1  8479  oneo  8508  oeoalem  8524  oeoelem  8526  nnaword1  8557  nnneo  8583  erov  8753  enrefg  8923  f1imaen  8956  mapxpen  9073  0sdom1dom  9148  acnlem  9960  djucomen  10090  nnadju  10110  infmap  10489  canthnumlem  10561  tskin  10672  tsksn  10673  tsk0  10676  gruxp  10720  gruina  10731  genpprecl  10914  addsrpr  10988  mulsrpr  10989  supsrlem  11024  mulrid  11132  00id  11310  mul02lem1  11311  ltneg  11639  leneg  11642  suble0  11653  div1  11833  nnaddcl  12170  nnmulcl  12171  nnge1  12175  nnsub  12191  2halves  12361  halfaddsub  12376  addltmul  12379  fcdmnn0fsuppg  12463  zleltp1  12544  nnaddm1cl  12551  zextlt  12568  eluzp1p1  12781  uzaddcl  12819  znq  12867  xrre  13086  xrre2  13087  fzshftral  13533  fraclt1  13724  expadd  14029  expmul  14032  sqmul  14044  expubnd  14103  bernneq  14154  faclbnd2  14216  faclbnd6  14224  hashgadd  14302  hashun2  14308  hashunsnggt  14319  hashssdif  14337  hashfun  14362  ccatlcan  14643  ccatrcan  14644  pfx2  14872  shftval3  15001  01sqrexlem1  15167  caubnd2  15283  bpoly2  15982  bpoly3  15983  fsumcube  15985  efexp  16028  efival  16079  cos01gt0  16118  odd2np1  16270  halfleoddlt  16291  omoe  16293  opeo  16294  divalglem5  16326  sqgcd  16491  nn0seqcvgd  16499  prmdvdssq  16647  phiprmpw  16705  eulerthlem2  16711  odzcllem  16722  pythagtriplem15  16759  pythagtriplem17  16761  pcelnn  16800  4sqlem3  16880  fullfunc  17834  fthfunc  17835  prfcl  18128  curf1cl  18153  curfcl  18157  hofcl  18184  odinv  19492  lsmelvalix  19572  dprdval  19936  lsp0  20962  lss0v  20970  zndvds0  21507  frlmlbs  21754  lindfres  21780  lmisfree  21799  coe1scl  22231  ntrin  23007  lpsscls  23087  restperf  23130  txuni2  23511  txopn  23548  elqtop2  23647  xkocnv  23760  ptcmp  24004  xblpnfps  24341  xblpnf  24342  bl2in  24346  unirnblps  24365  unirnbl  24366  blpnfctr  24382  dscopn  24519  bcthlem4  25285  minveclem2  25384  minveclem4  25390  icombl  25523  i1fadd  25654  i1fmul  25655  dvn1  25886  dvexp3  25940  plyconst  26169  plyid  26172  sincosq1eq  26479  sinord  26501  cxpp1  26647  cxpsqrtlem  26669  cxpsqrt  26670  angneg  26771  dcubic  26814  issqf  27104  ppiub  27173  bposlem1  27253  bposlem2  27254  bposlem9  27261  nosupno  27673  nosupfv  27676  noinfno  27688  noinffv  27691  scutval  27776  scutun12  27786  cuteq0  27811  cuteq1  27813  cofcut1  27900  cofcutr  27904  addscut2  27959  sleadd1  27969  addsuniflem  27981  addsasslem1  27983  addsasslem2  27984  negscut2  28020  mulsproplem12  28107  mulscut2  28113  divs1  28184  precsexlem10  28195  precsexlem11  28196  bdayon  28255  n0s0suc  28320  nnzsubs  28362  zmulscld  28374  elzs12i  28450  axlowdimlem6  29001  axlowdimlem14  29009  axcontlem2  29019  pthdlem2  29822  0ewlk  30170  ipasslem1  30887  ipasslem2  30888  ipasslem11  30896  minvecolem2  30931  minvecolem3  30932  minvecolem4  30936  shsva  31376  h1datomi  31637  lnfnmuli  32100  leopsq  32185  nmopleid  32195  opsqrlem6  32201  pjnmopi  32204  hstle  32286  csmdsymi  32390  atcvatlem  32441  dpfrac1  32952  cshf1o  33023  cycpmconjslem2  33216  rspidlid  33435  elsx  34330  dya2iocnrect  34417  r1omhf  35241  cvmliftphtlem  35490  satfv1  35536  satffunlem1lem2  35576  satffunlem1  35580  wlimeq12  35990  fvray  36314  fvline  36317  tailfb  36550  uncov  37771  tan2h  37782  matunitlindflem1  37786  matunitlindflem2  37787  poimirlem32  37822  mblfinlem4  37830  mbfresfi  37836  mbfposadd  37837  itg2addnc  37844  ftc1anclem5  37867  ftc1anclem8  37870  dvasin  37874  heiborlem7  37987  igenidl  38233  atlatmstc  39614  dihglblem2N  41589  eldioph4b  43090  diophren  43092  rmxp1  43211  rmyp1  43212  rmxm1  43213  rmym1  43214  dfgric2  48198  gpgov  48325  dig0  48889  i0oii  49202  iinfconstbas  49348  onetansqsecsq  50043  cotsqcscsq  50044