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 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  1454  mp3an23  1455  mp3anl3  1459  el3v3  3489  opelxp  5721  ov  7577  ovmpoa  7588  ovmpo  7593  frecseq123  8307  oaword1  8590  oneo  8619  oeoalem  8634  oeoelem  8636  nnaword1  8667  nnneo  8693  erov  8854  enrefg  9024  f1imaen  9057  mapxpen  9183  0sdom1dom  9274  acnlem  10088  djucomen  10218  nnadju  10238  infmap  10616  canthnumlem  10688  tskin  10799  tsksn  10800  tsk0  10803  gruxp  10847  gruina  10858  genpprecl  11041  addsrpr  11115  mulsrpr  11116  supsrlem  11151  mulrid  11259  00id  11436  mul02lem1  11437  ltneg  11763  leneg  11766  suble0  11777  div1  11957  nnaddcl  12289  nnmulcl  12290  nnge1  12294  nnsub  12310  2halves  12494  halfaddsub  12499  addltmul  12502  fcdmnn0fsuppg  12586  zleltp1  12668  nnaddm1cl  12675  zextlt  12692  eluzp1p1  12906  uzaddcl  12946  znq  12994  xrre  13211  xrre2  13212  fzshftral  13655  fraclt1  13842  expadd  14145  expmul  14148  sqmul  14159  expubnd  14217  bernneq  14268  faclbnd2  14330  faclbnd6  14338  hashgadd  14416  hashun2  14422  hashunsnggt  14433  hashssdif  14451  hashfun  14476  ccatlcan  14756  ccatrcan  14757  pfx2  14986  shftval3  15115  01sqrexlem1  15281  caubnd2  15396  bpoly2  16093  bpoly3  16094  fsumcube  16096  efexp  16137  efival  16188  cos01gt0  16227  odd2np1  16378  halfleoddlt  16399  omoe  16401  opeo  16402  divalglem5  16434  sqgcd  16599  nn0seqcvgd  16607  prmdvdssq  16755  phiprmpw  16813  eulerthlem2  16819  odzcllem  16830  pythagtriplem15  16867  pythagtriplem17  16869  pcelnn  16908  4sqlem3  16988  fullfunc  17953  fthfunc  17954  prfcl  18248  curf1cl  18273  curfcl  18277  hofcl  18304  odinv  19579  lsmelvalix  19659  dprdval  20023  lsp0  21007  lss0v  21015  zndvds0  21569  frlmlbs  21817  lindfres  21843  lmisfree  21862  coe1scl  22290  ntrin  23069  lpsscls  23149  restperf  23192  txuni2  23573  txopn  23610  elqtop2  23709  xkocnv  23822  ptcmp  24066  xblpnfps  24405  xblpnf  24406  bl2in  24410  unirnblps  24429  unirnbl  24430  blpnfctr  24446  dscopn  24586  bcthlem4  25361  minveclem2  25460  minveclem4  25466  icombl  25599  i1fadd  25730  i1fmul  25731  dvn1  25962  dvexp3  26016  plyconst  26245  plyid  26248  sincosq1eq  26554  sinord  26576  cxpp1  26722  cxpsqrtlem  26744  cxpsqrt  26745  angneg  26846  dcubic  26889  issqf  27179  ppiub  27248  bposlem1  27328  bposlem2  27329  bposlem9  27336  nosupno  27748  nosupfv  27751  noinfno  27763  noinffv  27766  scutval  27845  scutun12  27855  cuteq0  27877  cuteq1  27878  cofcut1  27954  cofcutr  27958  addscut2  28012  sleadd1  28022  addsuniflem  28034  addsasslem1  28036  addsasslem2  28037  negscut2  28072  mulsproplem12  28153  mulscut2  28159  divs1  28229  precsexlem10  28240  precsexlem11  28241  n0s0suc  28345  nnzsubs  28371  zmulscld  28383  axlowdimlem6  28962  axlowdimlem14  28970  axcontlem2  28980  pthdlem2  29788  0ewlk  30133  ipasslem1  30850  ipasslem2  30851  ipasslem11  30859  minvecolem2  30894  minvecolem3  30895  minvecolem4  30899  shsva  31339  h1datomi  31600  lnfnmuli  32063  leopsq  32148  nmopleid  32158  opsqrlem6  32164  pjnmopi  32167  hstle  32249  csmdsymi  32353  atcvatlem  32404  dpfrac1  32874  cshf1o  32947  cycpmconjslem2  33175  rspidlid  33403  elsx  34195  dya2iocnrect  34283  cvmliftphtlem  35322  satfv1  35368  satffunlem1lem2  35408  satffunlem1  35412  wlimeq12  35820  fvray  36142  fvline  36145  tailfb  36378  uncov  37608  tan2h  37619  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem32  37659  mblfinlem4  37667  mbfresfi  37673  mbfposadd  37674  itg2addnc  37681  ftc1anclem5  37704  ftc1anclem8  37707  dvasin  37711  heiborlem7  37824  igenidl  38070  atlatmstc  39320  dihglblem2N  41296  2xp3dxp2ge1d  42242  factwoffsmonot  42243  eldioph4b  42822  diophren  42824  rmxp1  42944  rmyp1  42945  rmxm1  42946  rmym1  42947  dfgric2  47884  gpgov  48001  dig0  48527  i0oii  48817  onetansqsecsq  49280  cotsqcscsq  49281