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  3468  opelxp  5690  ov  7549  ovmpoa  7560  ovmpo  7565  frecseq123  8279  oaword1  8562  oneo  8591  oeoalem  8606  oeoelem  8608  nnaword1  8639  nnneo  8665  erov  8826  enrefg  8996  f1imaen  9029  mapxpen  9155  0sdom1dom  9244  acnlem  10060  djucomen  10190  nnadju  10210  infmap  10588  canthnumlem  10660  tskin  10771  tsksn  10772  tsk0  10775  gruxp  10819  gruina  10830  genpprecl  11013  addsrpr  11087  mulsrpr  11088  supsrlem  11123  mulrid  11231  00id  11408  mul02lem1  11409  ltneg  11735  leneg  11738  suble0  11749  div1  11929  nnaddcl  12261  nnmulcl  12262  nnge1  12266  nnsub  12282  2halves  12457  halfaddsub  12472  addltmul  12475  fcdmnn0fsuppg  12559  zleltp1  12641  nnaddm1cl  12648  zextlt  12665  eluzp1p1  12878  uzaddcl  12918  znq  12966  xrre  13183  xrre2  13184  fzshftral  13630  fraclt1  13817  expadd  14120  expmul  14123  sqmul  14135  expubnd  14194  bernneq  14245  faclbnd2  14307  faclbnd6  14315  hashgadd  14393  hashun2  14399  hashunsnggt  14410  hashssdif  14428  hashfun  14453  ccatlcan  14734  ccatrcan  14735  pfx2  14964  shftval3  15093  01sqrexlem1  15259  caubnd2  15374  bpoly2  16071  bpoly3  16072  fsumcube  16074  efexp  16117  efival  16168  cos01gt0  16207  odd2np1  16358  halfleoddlt  16379  omoe  16381  opeo  16382  divalglem5  16414  sqgcd  16579  nn0seqcvgd  16587  prmdvdssq  16735  phiprmpw  16793  eulerthlem2  16799  odzcllem  16810  pythagtriplem15  16847  pythagtriplem17  16849  pcelnn  16888  4sqlem3  16968  fullfunc  17919  fthfunc  17920  prfcl  18213  curf1cl  18238  curfcl  18242  hofcl  18269  odinv  19540  lsmelvalix  19620  dprdval  19984  lsp0  20964  lss0v  20972  zndvds0  21509  frlmlbs  21755  lindfres  21781  lmisfree  21800  coe1scl  22222  ntrin  22997  lpsscls  23077  restperf  23120  txuni2  23501  txopn  23538  elqtop2  23637  xkocnv  23750  ptcmp  23994  xblpnfps  24332  xblpnf  24333  bl2in  24337  unirnblps  24356  unirnbl  24357  blpnfctr  24373  dscopn  24510  bcthlem4  25277  minveclem2  25376  minveclem4  25382  icombl  25515  i1fadd  25646  i1fmul  25647  dvn1  25878  dvexp3  25932  plyconst  26161  plyid  26164  sincosq1eq  26471  sinord  26493  cxpp1  26639  cxpsqrtlem  26661  cxpsqrt  26662  angneg  26763  dcubic  26806  issqf  27096  ppiub  27165  bposlem1  27245  bposlem2  27246  bposlem9  27253  nosupno  27665  nosupfv  27668  noinfno  27680  noinffv  27683  scutval  27762  scutun12  27772  cuteq0  27794  cuteq1  27795  cofcut1  27871  cofcutr  27875  addscut2  27929  sleadd1  27939  addsuniflem  27951  addsasslem1  27953  addsasslem2  27954  negscut2  27989  mulsproplem12  28070  mulscut2  28076  divs1  28146  precsexlem10  28157  precsexlem11  28158  n0s0suc  28262  nnzsubs  28288  zmulscld  28300  axlowdimlem6  28872  axlowdimlem14  28880  axcontlem2  28890  pthdlem2  29696  0ewlk  30041  ipasslem1  30758  ipasslem2  30759  ipasslem11  30767  minvecolem2  30802  minvecolem3  30803  minvecolem4  30807  shsva  31247  h1datomi  31508  lnfnmuli  31971  leopsq  32056  nmopleid  32066  opsqrlem6  32072  pjnmopi  32075  hstle  32157  csmdsymi  32261  atcvatlem  32312  dpfrac1  32812  cshf1o  32884  cycpmconjslem2  33112  rspidlid  33336  elsx  34171  dya2iocnrect  34259  cvmliftphtlem  35285  satfv1  35331  satffunlem1lem2  35371  satffunlem1  35375  wlimeq12  35783  fvray  36105  fvline  36108  tailfb  36341  uncov  37571  tan2h  37582  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem32  37622  mblfinlem4  37630  mbfresfi  37636  mbfposadd  37637  itg2addnc  37644  ftc1anclem5  37667  ftc1anclem8  37670  dvasin  37674  heiborlem7  37787  igenidl  38033  atlatmstc  39283  dihglblem2N  41259  2xp3dxp2ge1d  42200  factwoffsmonot  42201  eldioph4b  42781  diophren  42783  rmxp1  42903  rmyp1  42904  rmxm1  42905  rmym1  42906  dfgric2  47876  gpgov  47994  dig0  48534  i0oii  48842  iinfconstbas  48981  onetansqsecsq  49573  cotsqcscsq  49574