Theorem mp3an3 1473

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  mp3an13  1475  mp3an23  1476  mp3anl3  1480  el3v3  3465  opelxp  5685  ov  7542  ovmpoa  7553  ovmpo  7558  frecseq123  8265  oaword1  8523  oneo  8552  oeoalem  8568  oeoelem  8570  nnaword1  8601  nnneo  8627  erov  8798  enrefg  8967  f1imaen  9000  mapxpen  9117  0sdom1dom  9192  acnlem  10006  djucomen  10136  nnadju  10156  infmap  10536  canthnumlem  10608  tskin  10719  tsksn  10720  tsk0  10723  gruxp  10767  gruina  10778  genpprecl  10961  addsrpr  11035  mulsrpr  11036  supsrlem  11071  mulrid  11181  00id  11360  mul02lem1  11361  ltneg  11689  leneg  11692  suble0  11703  div1  11882  nnaddcl  12235  nnmulcl  12236  nnge1  12243  nnsub  12259  2halves  12441  halfaddsub  12456  addltmul  12459  fcdmnn0fsuppg  12543  zleltp1  12624  nnaddm1cl  12632  zextlt  12649  eluzp1p1  12869  uzaddcl  12907  znq  12955  xrre  13174  xrre2  13175  fzshftral  13622  fraclt1  13814  expadd  14119  expmul  14122  sqmul  14134  expubnd  14193  bernneq  14244  faclbnd2  14306  faclbnd6  14314  hashgadd  14392  hashun2  14398  hashunsnggt  14409  hashssdif  14427  hashfun  14452  ccatlcan  14733  ccatrcan  14734  pfx2  14962  shftval3  15091  01sqrexlem1  15271  caubnd2  15387  bpoly2  16089  bpoly3  16090  fsumcube  16092  efexp  16135  efival  16186  cos01gt0  16225  odd2np1  16377  halfleoddlt  16398  omoe  16400  opeo  16401  divalglem5  16433  sqgcd  16598  nn0seqcvgd  16606  prmdvdssq  16755  phiprmpw  16813  eulerthlem2  16819  odzcllem  16830  pythagtriplem15  16867  pythagtriplem17  16869  pcelnn  16908  4sqlem3  16988  fullfunc  17943  fthfunc  17944  prfcl  18237  curf1cl  18262  curfcl  18266  hofcl  18293  odinv  19603  lsmelvalix  19683  dprdval  20047  lsp0  21078  lss0v  21085  zndvds0  21604  frlmlbs  21851  lindfres  21877  lmisfree  21896  coe1scl  22352  ntrin  23123  lpsscls  23203  restperf  23246  txuni2  23627  txopn  23664  elqtop2  23763  xkocnv  23876  ptcmp  24120  xblpnfps  24457  xblpnf  24458  bl2in  24462  unirnblps  24481  unirnbl  24482  blpnfctr  24498  dscopn  24635  bcthlem4  25391  minveclem2  25490  minveclem4  25496  icombl  25628  i1fadd  25759  i1fmul  25760  dvn1  25990  dvexp3  26042  plyconst  26268  plyid  26271  sincosq1eq  26579  sinord  26601  cxpp1  26747  cxpsqrtlem  26769  cxpsqrt  26770  angneg  26870  dcubic  26913  issqf  27202  ppiub  27270  bposlem1  27350  bposlem2  27351  bposlem9  27358  nosupno  27769  nosupfv  27772  noinfno  27784  noinffv  27787  cutsval  27875  cutsun12  27885  cuteq0  27910  cuteq1  27912  cofcut1  28015  cofcutr  28019  addcuts2  28074  leadds1  28084  addsuniflem  28096  addsasslem1  28098  addsasslem2  28099  negcut2  28135  mulsproplem12  28222  mulcut2  28228  divs1  28299  precsexlem10  28311  precsexlem11  28312  bdayons  28371  n0s0suc  28437  nnzsubs  28480  zmulscld  28492  elz12si  28568  axlowdimlem6  29150  axlowdimlem14  29158  axcontlem2  29168  pthdlem2  29970  0ewlk  30318  ipasslem1  31036  ipasslem2  31037  ipasslem11  31045  minvecolem2  31080  minvecolem3  31081  minvecolem4  31085  shsva  31525  h1datomi  31786  lnfnmuli  32249  leopsq  32334  nmopleid  32344  opsqrlem6  32350  pjnmopi  32353  hstle  32435  csmdsymi  32539  atcvatlem  32590  dpfrac1  33071  cshf1o  33142  rspidlid  33563  elsx  34493  dya2iocnrect  34580  r1omhf  35406  cvmliftphtlem  35672  satfv1  35718  satffunlem1lem2  35758  satffunlem1  35762  wlimeq12  36172  fvray  36496  fvline  36499  tailfb  36742  ttc0elw  36892  uncov  38105  tan2h  38116  matunitlindflem1  38120  matunitlindflem2  38121  poimirlem32  38156  mblfinlem4  38164  mbfresfi  38170  mbfposadd  38171  itg2addnc  38178  ftc1anclem5  38201  ftc1anclem8  38204  dvasin  38208  heiborlem7  38321  igenidl  38567  atlatmstc  39948  dihglblem2N  41923  eldioph4b  43393  diophren  43395  rmxp1  43514  rmyp1  43515  rmxm1  43516  rmym1  43517  dfgric2  48542  gpgov  48669  dig0  49233  i0oii  49546  iinfconstbas  49692  onetansqsecsq  50387  cotsqcscsq  50388