Theorem mp3an3 1453

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 1122	. 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  1455  mp3an23  1456  mp3anl3  1460  el3v3  3436  opelxp  5656  ov  7500  ovmpoa  7511  ovmpo  7516  frecseq123  8221  oaword1  8476  oneo  8505  oeoalem  8521  oeoelem  8523  nnaword1  8554  nnneo  8580  erov  8750  enrefg  8920  f1imaen  8953  mapxpen  9070  0sdom1dom  9145  acnlem  9959  djucomen  10089  nnadju  10109  infmap  10488  canthnumlem  10560  tskin  10671  tsksn  10672  tsk0  10675  gruxp  10719  gruina  10730  genpprecl  10913  addsrpr  10987  mulsrpr  10988  supsrlem  11023  mulrid  11131  00id  11310  mul02lem1  11311  ltneg  11639  leneg  11642  suble0  11653  div1  11833  nnaddcl  12186  nnmulcl  12187  nnge1  12194  nnsub  12210  2halves  12384  halfaddsub  12399  addltmul  12402  fcdmnn0fsuppg  12486  zleltp1  12567  nnaddm1cl  12575  zextlt  12592  eluzp1p1  12805  uzaddcl  12843  znq  12891  xrre  13110  xrre2  13111  fzshftral  13558  fraclt1  13750  expadd  14055  expmul  14058  sqmul  14070  expubnd  14129  bernneq  14180  faclbnd2  14242  faclbnd6  14250  hashgadd  14328  hashun2  14334  hashunsnggt  14345  hashssdif  14363  hashfun  14388  ccatlcan  14669  ccatrcan  14670  pfx2  14898  shftval3  15027  01sqrexlem1  15193  caubnd2  15309  bpoly2  16011  bpoly3  16012  fsumcube  16014  efexp  16057  efival  16108  cos01gt0  16147  odd2np1  16299  halfleoddlt  16320  omoe  16322  opeo  16323  divalglem5  16355  sqgcd  16520  nn0seqcvgd  16528  prmdvdssq  16677  phiprmpw  16735  eulerthlem2  16741  odzcllem  16752  pythagtriplem15  16789  pythagtriplem17  16791  pcelnn  16830  4sqlem3  16910  fullfunc  17864  fthfunc  17865  prfcl  18158  curf1cl  18183  curfcl  18187  hofcl  18214  odinv  19525  lsmelvalix  19605  dprdval  19969  lsp0  20993  lss0v  21000  zndvds0  21519  frlmlbs  21766  lindfres  21792  lmisfree  21811  coe1scl  22240  ntrin  23014  lpsscls  23094  restperf  23137  txuni2  23518  txopn  23555  elqtop2  23654  xkocnv  23767  ptcmp  24011  xblpnfps  24348  xblpnf  24349  bl2in  24353  unirnblps  24372  unirnbl  24373  blpnfctr  24389  dscopn  24526  bcthlem4  25282  minveclem2  25381  minveclem4  25387  icombl  25519  i1fadd  25650  i1fmul  25651  dvn1  25881  dvexp3  25933  plyconst  26159  plyid  26162  sincosq1eq  26464  sinord  26486  cxpp1  26632  cxpsqrtlem  26654  cxpsqrt  26655  angneg  26755  dcubic  26798  issqf  27087  ppiub  27155  bposlem1  27235  bposlem2  27236  bposlem9  27243  nosupno  27655  nosupfv  27658  noinfno  27670  noinffv  27673  cutsval  27760  cutsun12  27770  cuteq0  27795  cuteq1  27797  cofcut1  27900  cofcutr  27904  addcuts2  27959  leadds1  27969  addsuniflem  27981  addsasslem1  27983  addsasslem2  27984  negcut2  28020  mulsproplem12  28107  mulcut2  28113  divs1  28184  precsexlem10  28196  precsexlem11  28197  bdayons  28256  n0s0suc  28322  nnzsubs  28365  zmulscld  28377  elz12si  28453  axlowdimlem6  29004  axlowdimlem14  29012  axcontlem2  29022  pthdlem2  29824  0ewlk  30172  ipasslem1  30890  ipasslem2  30891  ipasslem11  30899  minvecolem2  30934  minvecolem3  30935  minvecolem4  30939  shsva  31379  h1datomi  31640  lnfnmuli  32103  leopsq  32188  nmopleid  32198  opsqrlem6  32204  pjnmopi  32207  hstle  32289  csmdsymi  32393  atcvatlem  32444  dpfrac1  32939  cshf1o  33010  cycpmconjslem2  33204  rspidlid  33423  elsx  34326  dya2iocnrect  34413  r1omhf  35237  cvmliftphtlem  35487  satfv1  35533  satffunlem1lem2  35573  satffunlem1  35577  wlimeq12  35987  fvray  36311  fvline  36314  tailfb  36547  ttc0elw  36697  uncov  37910  tan2h  37921  matunitlindflem1  37925  matunitlindflem2  37926  poimirlem32  37961  mblfinlem4  37969  mbfresfi  37975  mbfposadd  37976  itg2addnc  37983  ftc1anclem5  38006  ftc1anclem8  38009  dvasin  38013  heiborlem7  38126  igenidl  38372  atlatmstc  39753  dihglblem2N  41728  eldioph4b  43227  diophren  43229  rmxp1  43348  rmyp1  43349  rmxm1  43350  rmym1  43351  dfgric2  48379  gpgov  48506  dig0  49070  i0oii  49383  iinfconstbas  49529  onetansqsecsq  50224  cotsqcscsq  50225