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 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 206  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an13  1451  mp3an23  1452  mp3anl3  1456  opelxp  5712  ov  7555  ovmpoa  7566  ovmpo  7571  frecseq123  8273  oaword1  8558  oneo  8587  oeoalem  8602  oeoelem  8604  nnaword1  8635  nnneo  8660  erov  8814  enrefg  8986  f1imaen  9018  mapxpen  9149  0sdom1dom  9244  acnlem  10049  djucomen  10178  nnadju  10198  infmap  10577  canthnumlem  10649  tskin  10760  tsksn  10761  tsk0  10764  gruxp  10808  gruina  10819  genpprecl  11002  addsrpr  11076  mulsrpr  11077  supsrlem  11112  mulrid  11219  00id  11396  mul02lem1  11397  ltneg  11721  leneg  11724  suble0  11735  div1  11910  nnaddcl  12242  nnmulcl  12243  nnge1  12247  nnsub  12263  2halves  12447  halfaddsub  12452  addltmul  12455  fcdmnn0fsuppg  12538  zleltp1  12620  nnaddm1cl  12626  zextlt  12643  eluzp1p1  12857  uzaddcl  12895  znq  12943  xrre  13155  xrre2  13156  fzshftral  13596  fraclt1  13774  expadd  14077  expmul  14080  sqmul  14091  expubnd  14149  bernneq  14199  faclbnd2  14258  faclbnd6  14266  hashgadd  14344  hashun2  14350  hashunsnggt  14361  hashssdif  14379  hashfun  14404  ccatlcan  14675  ccatrcan  14676  pfx2  14905  shftval3  15030  01sqrexlem1  15196  caubnd2  15311  bpoly2  16008  bpoly3  16009  fsumcube  16011  efexp  16051  efival  16102  cos01gt0  16141  odd2np1  16291  halfleoddlt  16312  omoe  16314  opeo  16315  divalglem5  16347  sqgcd  16509  nn0seqcvgd  16514  prmdvdssq  16662  phiprmpw  16716  eulerthlem2  16722  odzcllem  16732  pythagtriplem15  16769  pythagtriplem17  16771  pcelnn  16810  4sqlem3  16890  fullfunc  17866  fthfunc  17867  prfcl  18165  curf1cl  18191  curfcl  18195  hofcl  18222  odinv  19477  lsmelvalix  19557  dprdval  19921  lsp0  20852  lss0v  20859  zndvds0  21415  frlmlbs  21661  lindfres  21687  lmisfree  21706  coe1scl  22128  ntrin  22884  lpsscls  22964  restperf  23007  txuni2  23388  txopn  23425  elqtop2  23524  xkocnv  23637  ptcmp  23881  xblpnfps  24220  xblpnf  24221  bl2in  24225  unirnblps  24244  unirnbl  24245  blpnfctr  24261  dscopn  24401  bcthlem4  25174  minveclem2  25273  minveclem4  25279  icombl  25412  i1fadd  25543  i1fmul  25544  dvn1  25775  dvexp3  25829  plyconst  26057  plyid  26060  sincosq1eq  26361  sinord  26382  cxpp1  26527  cxpsqrtlem  26549  cxpsqrt  26550  angneg  26648  dcubic  26691  issqf  26980  ppiub  27049  bposlem1  27129  bposlem2  27130  bposlem9  27137  nosupno  27548  nosupfv  27551  noinfno  27563  noinffv  27566  scutval  27645  scutun12  27655  cuteq0  27677  cuteq1  27678  cofcut1  27752  cofcutr  27756  addscut2  27808  sleadd1  27818  addsuniflem  27830  addsasslem1  27832  addsasslem2  27833  negscut2  27864  mulsproplem12  27939  mulscut2  27945  divs1  28015  precsexlem10  28026  precsexlem11  28027  axlowdimlem6  28637  axlowdimlem14  28645  axcontlem2  28655  pthdlem2  29457  0ewlk  29799  ipasslem1  30516  ipasslem2  30517  ipasslem11  30525  minvecolem2  30560  minvecolem3  30561  minvecolem4  30565  shsva  31005  h1datomi  31266  lnfnmuli  31729  leopsq  31814  nmopleid  31824  opsqrlem6  31830  pjnmopi  31833  hstle  31915  csmdsymi  32019  atcvatlem  32070  dpfrac1  32490  cshf1o  32558  cycpmconjslem2  32749  rspidlid  32926  elsx  33655  dya2iocnrect  33743  cvmliftphtlem  34771  satfv1  34817  satffunlem1lem2  34857  satffunlem1  34861  wlimeq12  35260  fvray  35582  fvline  35585  tailfb  35725  uncov  36932  tan2h  36943  matunitlindflem1  36947  matunitlindflem2  36948  poimirlem32  36983  mblfinlem4  36991  mbfresfi  36997  mbfposadd  36998  itg2addnc  37005  ftc1anclem5  37028  ftc1anclem8  37031  dvasin  37035  heiborlem7  37148  igenidl  37394  el3v3  37552  atlatmstc  38652  dihglblem2N  40628  2xp3dxp2ge1d  41488  factwoffsmonot  41489  eldioph4b  42011  diophren  42013  rmxp1  42133  rmyp1  42134  rmxm1  42135  rmym1  42136  dig0  47453  i0oii  47713  onetansqsecsq  47967  cotsqcscsq  47968