Theorem mp3an3 1452

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an13  1454  mp3an23  1455  mp3anl3  1459  el3v3  3456  opelxp  5674  ov  7533  ovmpoa  7544  ovmpo  7549  frecseq123  8261  oaword1  8516  oneo  8545  oeoalem  8560  oeoelem  8562  nnaword1  8593  nnneo  8619  erov  8787  enrefg  8955  f1imaen  8988  mapxpen  9107  0sdom1dom  9185  acnlem  10001  djucomen  10131  nnadju  10151  infmap  10529  canthnumlem  10601  tskin  10712  tsksn  10713  tsk0  10716  gruxp  10760  gruina  10771  genpprecl  10954  addsrpr  11028  mulsrpr  11029  supsrlem  11064  mulrid  11172  00id  11349  mul02lem1  11350  ltneg  11678  leneg  11681  suble0  11692  div1  11872  nnaddcl  12209  nnmulcl  12210  nnge1  12214  nnsub  12230  2halves  12400  halfaddsub  12415  addltmul  12418  fcdmnn0fsuppg  12502  zleltp1  12584  nnaddm1cl  12591  zextlt  12608  eluzp1p1  12821  uzaddcl  12863  znq  12911  xrre  13129  xrre2  13130  fzshftral  13576  fraclt1  13764  expadd  14069  expmul  14072  sqmul  14084  expubnd  14143  bernneq  14194  faclbnd2  14256  faclbnd6  14264  hashgadd  14342  hashun2  14348  hashunsnggt  14359  hashssdif  14377  hashfun  14402  ccatlcan  14683  ccatrcan  14684  pfx2  14913  shftval3  15042  01sqrexlem1  15208  caubnd2  15324  bpoly2  16023  bpoly3  16024  fsumcube  16026  efexp  16069  efival  16120  cos01gt0  16159  odd2np1  16311  halfleoddlt  16332  omoe  16334  opeo  16335  divalglem5  16367  sqgcd  16532  nn0seqcvgd  16540  prmdvdssq  16688  phiprmpw  16746  eulerthlem2  16752  odzcllem  16763  pythagtriplem15  16800  pythagtriplem17  16802  pcelnn  16841  4sqlem3  16921  fullfunc  17870  fthfunc  17871  prfcl  18164  curf1cl  18189  curfcl  18193  hofcl  18220  odinv  19491  lsmelvalix  19571  dprdval  19935  lsp0  20915  lss0v  20923  zndvds0  21460  frlmlbs  21706  lindfres  21732  lmisfree  21751  coe1scl  22173  ntrin  22948  lpsscls  23028  restperf  23071  txuni2  23452  txopn  23489  elqtop2  23588  xkocnv  23701  ptcmp  23945  xblpnfps  24283  xblpnf  24284  bl2in  24288  unirnblps  24307  unirnbl  24308  blpnfctr  24324  dscopn  24461  bcthlem4  25227  minveclem2  25326  minveclem4  25332  icombl  25465  i1fadd  25596  i1fmul  25597  dvn1  25828  dvexp3  25882  plyconst  26111  plyid  26114  sincosq1eq  26421  sinord  26443  cxpp1  26589  cxpsqrtlem  26611  cxpsqrt  26612  angneg  26713  dcubic  26756  issqf  27046  ppiub  27115  bposlem1  27195  bposlem2  27196  bposlem9  27203  nosupno  27615  nosupfv  27618  noinfno  27630  noinffv  27633  scutval  27712  scutun12  27722  cuteq0  27744  cuteq1  27746  cofcut1  27828  cofcutr  27832  addscut2  27886  sleadd1  27896  addsuniflem  27908  addsasslem1  27910  addsasslem2  27911  negscut2  27946  mulsproplem12  28030  mulscut2  28036  divs1  28107  precsexlem10  28118  precsexlem11  28119  bdayon  28173  n0s0suc  28234  nnzsubs  28273  zmulscld  28285  axlowdimlem6  28874  axlowdimlem14  28882  axcontlem2  28892  pthdlem2  29698  0ewlk  30043  ipasslem1  30760  ipasslem2  30761  ipasslem11  30769  minvecolem2  30804  minvecolem3  30805  minvecolem4  30809  shsva  31249  h1datomi  31510  lnfnmuli  31973  leopsq  32058  nmopleid  32068  opsqrlem6  32074  pjnmopi  32077  hstle  32159  csmdsymi  32263  atcvatlem  32314  dpfrac1  32812  cshf1o  32884  cycpmconjslem2  33112  rspidlid  33346  elsx  34184  dya2iocnrect  34272  cvmliftphtlem  35304  satfv1  35350  satffunlem1lem2  35390  satffunlem1  35394  wlimeq12  35807  fvray  36129  fvline  36132  tailfb  36365  uncov  37595  tan2h  37606  matunitlindflem1  37610  matunitlindflem2  37611  poimirlem32  37646  mblfinlem4  37654  mbfresfi  37660  mbfposadd  37661  itg2addnc  37668  ftc1anclem5  37691  ftc1anclem8  37694  dvasin  37698  heiborlem7  37811  igenidl  38057  atlatmstc  39312  dihglblem2N  41288  eldioph4b  42799  diophren  42801  rmxp1  42921  rmyp1  42922  rmxm1  42923  rmym1  42924  dfgric2  47915  gpgov  48033  dig0  48595  i0oii  48908  iinfconstbas  49055  onetansqsecsq  49750  cotsqcscsq  49751