Theorem mp3an3 1477

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3an13  1479  mp3an23  1480  mp3anl3  1484  el3v3  3462  opelxp  5697  ov  7554  ovmpoa  7565  ovmpo  7570  frecseq123  8278  oaword1  8536  oneo  8565  oeoalem  8581  oeoelem  8583  nnaword1  8614  nnneo  8640  erov  8811  enrefg  8980  f1imaen  9013  mapxpen  9130  0sdom1dom  9205  acnlem  10031  djucomen  10160  nnadju  10180  infmap  10560  canthnumlem  10632  tskin  10743  tsksn  10744  tsk0  10747  gruxp  10791  gruina  10802  genpprecl  10985  addsrpr  11059  mulsrpr  11060  supsrlem  11095  mulrid  11205  00id  11384  mul02lem1  11385  ltneg  11713  leneg  11716  suble0  11727  div1  11903  nnaddcl  12255  nnmulcl  12256  nnge1  12263  nnsub  12279  2halves  12461  halfaddsub  12476  addltmul  12479  fcdmnn0fsuppg  12563  zleltp1  12644  nnaddm1cl  12652  zextlt  12669  eluzp1p1  12889  uzaddcl  12927  znq  12975  xrre  13194  xrre2  13195  fzshftral  13642  fraclt1  13834  expadd  14139  expmul  14142  sqmul  14154  expubnd  14213  bernneq  14264  faclbnd2  14326  faclbnd6  14334  hashgadd  14412  hashun2  14418  hashunsnggt  14429  hashssdif  14448  hashfun  14473  ccatlcan  14754  ccatrcan  14755  pfx2  14983  shftval3  15112  01sqrexlem1  15292  caubnd2  15408  bpoly2  16110  bpoly3  16111  fsumcube  16113  efexp  16156  efival  16207  cos01gt0  16246  odd2np1  16398  halfleoddlt  16419  omoe  16421  opeo  16422  divalglem5  16454  sqgcd  16619  nn0seqcvgd  16627  prmdvdssq  16776  phiprmpw  16834  eulerthlem2  16840  odzcllem  16851  pythagtriplem15  16888  pythagtriplem17  16890  pcelnn  16929  4sqlem3  17009  fullfunc  17964  fthfunc  17965  prfcl  18258  curf1cl  18283  curfcl  18287  hofcl  18314  odinv  19630  lsmelvalix  19710  dprdval  20074  lsp0  21109  lss0v  21116  zndvds0  21679  frlmlbs  21926  lindfres  21952  lmisfree  21971  coe1scl  22427  ntrin  23197  lpsscls  23277  restperf  23320  txuni2  23701  txopn  23738  elqtop2  23837  xkocnv  23950  ptcmp  24194  xblpnfps  24531  xblpnf  24532  bl2in  24536  unirnblps  24555  unirnbl  24556  blpnfctr  24572  dscopn  24709  bcthlem4  25465  minveclem2  25564  minveclem4  25570  icombl  25702  i1fadd  25833  i1fmul  25834  dvn1  26064  dvexp3  26116  plyconst  26342  plyid  26345  sincosq1eq  26653  sinord  26675  cxpp1  26821  cxpsqrtlem  26843  cxpsqrt  26844  angneg  26944  dcubic  26987  issqf  27276  ppiub  27344  bposlem1  27424  bposlem2  27425  bposlem9  27432  nosupno  27843  nosupfv  27846  noinfno  27858  noinffv  27861  cutsval  27949  cutsun12  27959  cuteq0  27984  cuteq1  27986  cofcut1  28089  cofcutr  28093  addcuts2  28148  leadds1  28158  addsuniflem  28170  addsasslem1  28172  addsasslem2  28173  negcut2  28209  mulsproplem12  28296  mulcut2  28302  divs1  28373  precsexlem10  28385  precsexlem11  28386  bdayons  28445  n0s0suc  28511  nnzsubs  28554  zmulscld  28566  elz12si  28642  axlowdimlem6  29263  axlowdimlem14  29271  axcontlem2  29281  pthdlem2  30083  0ewlk  30431  ipasslem1  31149  ipasslem2  31150  ipasslem11  31158  minvecolem2  31193  minvecolem3  31194  minvecolem4  31198  shsva  31638  h1datomi  31899  lnfnmuli  32362  leopsq  32447  nmopleid  32457  opsqrlem6  32463  pjnmopi  32466  hstle  32548  csmdsymi  32652  atcvatlem  32703  dpfrac1  33177  cshf1o  33248  rspidlid  33655  elsx  34550  dya2iocnrect  34637  r1omhf  35464  cvmliftphtlem  35763  satfv1  35809  satffunlem1lem2  35849  satffunlem1  35853  wlimeq12  36263  fvray  36587  fvline  36590  tailfb  36832  ttc0elw  36982  uncov  38196  tan2h  38207  matunitlindflem1  38211  matunitlindflem2  38212  poimirlem32  38247  mblfinlem4  38255  mbfresfi  38261  mbfposadd  38262  itg2addnc  38269  ftc1anclem5  38292  ftc1anclem8  38295  dvasin  38299  heiborlem7  38412  igenidl  38658  atlatmstc  40039  dihglblem2N  42014  eldioph4b  43486  diophren  43488  rmxp1  43607  rmyp1  43608  rmxm1  43609  rmym1  43610  dfgric2  48625  gpgov  48752  dig0  49331  i0oii  49643  iinfconstbas  49789  onetansqsecsq  50484  cotsqcscsq  50485