Theorem mp3an3 1450

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 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  1452  mp3an23  1453  mp3anl3  1457  el3v3  3497  opelxp  5736  ov  7594  ovmpoa  7605  ovmpo  7610  frecseq123  8323  oaword1  8608  oneo  8637  oeoalem  8652  oeoelem  8654  nnaword1  8685  nnneo  8711  erov  8872  enrefg  9044  f1imaen  9077  mapxpen  9209  0sdom1dom  9301  acnlem  10117  djucomen  10247  nnadju  10267  infmap  10645  canthnumlem  10717  tskin  10828  tsksn  10829  tsk0  10832  gruxp  10876  gruina  10887  genpprecl  11070  addsrpr  11144  mulsrpr  11145  supsrlem  11180  mulrid  11288  00id  11465  mul02lem1  11466  ltneg  11790  leneg  11793  suble0  11804  div1  11984  nnaddcl  12316  nnmulcl  12317  nnge1  12321  nnsub  12337  2halves  12521  halfaddsub  12526  addltmul  12529  fcdmnn0fsuppg  12612  zleltp1  12694  nnaddm1cl  12700  zextlt  12717  eluzp1p1  12931  uzaddcl  12969  znq  13017  xrre  13231  xrre2  13232  fzshftral  13672  fraclt1  13853  expadd  14155  expmul  14158  sqmul  14169  expubnd  14227  bernneq  14278  faclbnd2  14340  faclbnd6  14348  hashgadd  14426  hashun2  14432  hashunsnggt  14443  hashssdif  14461  hashfun  14486  ccatlcan  14766  ccatrcan  14767  pfx2  14996  shftval3  15125  01sqrexlem1  15291  caubnd2  15406  bpoly2  16105  bpoly3  16106  fsumcube  16108  efexp  16149  efival  16200  cos01gt0  16239  odd2np1  16389  halfleoddlt  16410  omoe  16412  opeo  16413  divalglem5  16445  sqgcd  16609  nn0seqcvgd  16617  prmdvdssq  16765  phiprmpw  16823  eulerthlem2  16829  odzcllem  16839  pythagtriplem15  16876  pythagtriplem17  16878  pcelnn  16917  4sqlem3  16997  fullfunc  17973  fthfunc  17974  prfcl  18272  curf1cl  18298  curfcl  18302  hofcl  18329  odinv  19603  lsmelvalix  19683  dprdval  20047  lsp0  21030  lss0v  21038  zndvds0  21592  frlmlbs  21840  lindfres  21866  lmisfree  21885  coe1scl  22311  ntrin  23090  lpsscls  23170  restperf  23213  txuni2  23594  txopn  23631  elqtop2  23730  xkocnv  23843  ptcmp  24087  xblpnfps  24426  xblpnf  24427  bl2in  24431  unirnblps  24450  unirnbl  24451  blpnfctr  24467  dscopn  24607  bcthlem4  25380  minveclem2  25479  minveclem4  25485  icombl  25618  i1fadd  25749  i1fmul  25750  dvn1  25982  dvexp3  26036  plyconst  26265  plyid  26268  sincosq1eq  26572  sinord  26594  cxpp1  26740  cxpsqrtlem  26762  cxpsqrt  26763  angneg  26864  dcubic  26907  issqf  27197  ppiub  27266  bposlem1  27346  bposlem2  27347  bposlem9  27354  nosupno  27766  nosupfv  27769  noinfno  27781  noinffv  27784  scutval  27863  scutun12  27873  cuteq0  27895  cuteq1  27896  cofcut1  27972  cofcutr  27976  addscut2  28030  sleadd1  28040  addsuniflem  28052  addsasslem1  28054  addsasslem2  28055  negscut2  28090  mulsproplem12  28171  mulscut2  28177  divs1  28247  precsexlem10  28258  precsexlem11  28259  n0s0suc  28363  nnzsubs  28389  zmulscld  28401  axlowdimlem6  28980  axlowdimlem14  28988  axcontlem2  28998  pthdlem2  29804  0ewlk  30146  ipasslem1  30863  ipasslem2  30864  ipasslem11  30872  minvecolem2  30907  minvecolem3  30908  minvecolem4  30912  shsva  31352  h1datomi  31613  lnfnmuli  32076  leopsq  32161  nmopleid  32171  opsqrlem6  32177  pjnmopi  32180  hstle  32262  csmdsymi  32366  atcvatlem  32417  dpfrac1  32856  cshf1o  32929  cycpmconjslem2  33148  rspidlid  33368  elsx  34158  dya2iocnrect  34246  cvmliftphtlem  35285  satfv1  35331  satffunlem1lem2  35371  satffunlem1  35375  wlimeq12  35783  fvray  36105  fvline  36108  tailfb  36343  uncov  37561  tan2h  37572  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem32  37612  mblfinlem4  37620  mbfresfi  37626  mbfposadd  37627  itg2addnc  37634  ftc1anclem5  37657  ftc1anclem8  37660  dvasin  37664  heiborlem7  37777  igenidl  38023  atlatmstc  39275  dihglblem2N  41251  2xp3dxp2ge1d  42198  factwoffsmonot  42199  eldioph4b  42767  diophren  42769  rmxp1  42889  rmyp1  42890  rmxm1  42891  rmym1  42892  dfgric2  47768  dig0  48340  i0oii  48599  onetansqsecsq  48853  cotsqcscsq  48854