Theorem mp3an3 1446

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  mp3an13  1448  mp3an23  1449  mp3anl3  1453  opelxp  5594  ov  7297  ovmpoa  7308  ovmpo  7313  oaword1  8181  oneo  8210  oeoalem  8225  oeoelem  8227  nnaword1  8258  nnneo  8281  erov  8397  enrefg  8544  f1imaen  8574  mapxpen  8686  acnlem  9477  djucomen  9606  infmap  10001  canthnumlem  10073  tskin  10184  tsksn  10185  tsk0  10188  gruxp  10232  gruina  10243  genpprecl  10426  addsrpr  10500  mulsrpr  10501  supsrlem  10536  mulid1  10642  00id  10818  mul02lem1  10819  ltneg  11143  leneg  11146  suble0  11157  div1  11332  nnaddcl  11663  nnmulcl  11664  nnge1  11668  nnsub  11684  2halves  11868  halfaddsub  11873  addltmul  11876  zleltp1  12036  nnaddm1cl  12042  zextlt  12059  eluzp1p1  12273  uzaddcl  12307  znq  12355  xrre  12565  xrre2  12566  fzshftral  12998  fraclt1  13175  expadd  13474  expmul  13477  sqmul  13488  expubnd  13544  bernneq  13593  faclbnd2  13654  faclbnd6  13662  hashgadd  13741  hashun2  13747  hashunsnggt  13758  hashssdif  13776  hashfun  13801  ccatlcan  14083  ccatrcan  14084  pfx2  14312  shftval3  14438  sqrlem1  14605  caubnd2  14720  bpoly2  15414  bpoly3  15415  fsumcube  15417  efexp  15457  efival  15508  cos01gt0  15547  odd2np1  15693  halfleoddlt  15714  omoe  15716  opeo  15717  divalglem5  15751  gcdmultipleOLD  15903  sqgcd  15912  nn0seqcvgd  15917  phiprmpw  16116  eulerthlem2  16122  odzcllem  16132  pythagtriplem15  16169  pythagtriplem17  16171  pcelnn  16209  4sqlem3  16289  fullfunc  17179  fthfunc  17180  prfcl  17456  curf1cl  17481  curfcl  17485  hofcl  17512  odinv  18691  lsmelvalix  18769  dprdval  19128  lsp0  19784  lss0v  19791  coe1scl  20458  zndvds0  20700  frlmlbs  20944  lindfres  20970  lmisfree  20989  ntrin  21672  lpsscls  21752  restperf  21795  txuni2  22176  txopn  22213  elqtop2  22312  xkocnv  22425  ptcmp  22669  xblpnfps  23008  xblpnf  23009  bl2in  23013  unirnblps  23032  unirnbl  23033  blpnfctr  23049  dscopn  23186  bcthlem4  23933  minveclem2  24032  minveclem4  24038  icombl  24168  i1fadd  24299  i1fmul  24300  dvn1  24526  dvexp3  24578  plyconst  24799  plyid  24802  sincosq1eq  25101  sinord  25121  cxpp1  25266  cxpsqrtlem  25288  cxpsqrt  25289  angneg  25384  dcubic  25427  issqf  25716  ppiub  25783  bposlem1  25863  bposlem2  25864  bposlem9  25871  axlowdimlem6  26736  axlowdimlem14  26744  axcontlem2  26754  pthdlem2  27552  0ewlk  27896  ipasslem1  28611  ipasslem2  28612  ipasslem11  28620  minvecolem2  28655  minvecolem3  28656  minvecolem4  28660  shsva  29100  h1datomi  29361  lnfnmuli  29824  leopsq  29909  nmopleid  29919  opsqrlem6  29925  pjnmopi  29928  hstle  30010  csmdsymi  30114  atcvatlem  30165  dpfrac1  30572  cshf1o  30640  cycpmconjslem2  30801  elsx  31457  dya2iocnrect  31543  cvmliftphtlem  32568  satfv1  32614  satffunlem1lem2  32654  satffunlem1  32658  wlimeq12  33110  frecseq123  33123  nosupno  33207  nosupfv  33210  scutval  33269  scutun12  33275  fvray  33606  fvline  33609  tailfb  33729  uncov  34877  tan2h  34888  matunitlindflem1  34892  matunitlindflem2  34893  poimirlem32  34928  mblfinlem4  34936  mbfresfi  34942  mbfposadd  34943  itg2addnc  34950  ftc1anclem5  34975  ftc1anclem8  34978  dvasin  34982  heiborlem7  35099  igenidl  35345  el3v3  35498  atlatmstc  36459  dihglblem2N  38434  eldioph4b  39414  diophren  39416  rmxp1  39535  rmyp1  39536  rmxm1  39537  rmym1  39538  wepwso  39649  dig0  44673  onetansqsecsq  44867  cotsqcscsq  44868