Theorem mp3an3 1447

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  mp3an13  1449  mp3an23  1450  mp3anl3  1454  opelxp  5564  ov  7295  ovmpoa  7306  ovmpo  7311  oaword1  8194  oneo  8223  oeoalem  8238  oeoelem  8240  nnaword1  8271  nnneo  8294  erov  8410  enrefg  8572  f1imaen  8602  mapxpen  8718  acnlem  9521  djucomen  9650  nnadju  9670  infmap  10049  canthnumlem  10121  tskin  10232  tsksn  10233  tsk0  10236  gruxp  10280  gruina  10291  genpprecl  10474  addsrpr  10548  mulsrpr  10549  supsrlem  10584  mulid1  10690  00id  10866  mul02lem1  10867  ltneg  11191  leneg  11194  suble0  11205  div1  11380  nnaddcl  11710  nnmulcl  11711  nnge1  11715  nnsub  11731  2halves  11915  halfaddsub  11920  addltmul  11923  frnnn0fsuppg  12006  zleltp1  12085  nnaddm1cl  12091  zextlt  12108  eluzp1p1  12323  uzaddcl  12357  znq  12405  xrre  12616  xrre2  12617  fzshftral  13057  fraclt1  13234  expadd  13534  expmul  13537  sqmul  13548  expubnd  13604  bernneq  13653  faclbnd2  13714  faclbnd6  13722  hashgadd  13801  hashun2  13807  hashunsnggt  13818  hashssdif  13836  hashfun  13861  ccatlcan  14140  ccatrcan  14141  pfx2  14369  shftval3  14496  sqrlem1  14663  caubnd2  14778  bpoly2  15472  bpoly3  15473  fsumcube  15475  efexp  15515  efival  15566  cos01gt0  15605  odd2np1  15755  halfleoddlt  15776  omoe  15778  opeo  15779  divalglem5  15811  gcdmultipleOLD  15964  sqgcd  15974  nn0seqcvgd  15979  prmdvdssq  16127  phiprmpw  16181  eulerthlem2  16187  odzcllem  16197  pythagtriplem15  16234  pythagtriplem17  16236  pcelnn  16274  4sqlem3  16354  fullfunc  17248  fthfunc  17249  prfcl  17532  curf1cl  17557  curfcl  17561  hofcl  17588  odinv  18768  lsmelvalix  18846  dprdval  19206  lsp0  19862  lss0v  19869  zndvds0  20331  frlmlbs  20575  lindfres  20601  lmisfree  20620  coe1scl  21024  ntrin  21774  lpsscls  21854  restperf  21897  txuni2  22278  txopn  22315  elqtop2  22414  xkocnv  22527  ptcmp  22771  xblpnfps  23110  xblpnf  23111  bl2in  23115  unirnblps  23134  unirnbl  23135  blpnfctr  23151  dscopn  23288  bcthlem4  24040  minveclem2  24139  minveclem4  24145  icombl  24277  i1fadd  24408  i1fmul  24409  dvn1  24638  dvexp3  24690  plyconst  24915  plyid  24918  sincosq1eq  25217  sinord  25238  cxpp1  25383  cxpsqrtlem  25405  cxpsqrt  25406  angneg  25501  dcubic  25544  issqf  25833  ppiub  25900  bposlem1  25980  bposlem2  25981  bposlem9  25988  axlowdimlem6  26853  axlowdimlem14  26861  axcontlem2  26871  pthdlem2  27669  0ewlk  28011  ipasslem1  28726  ipasslem2  28727  ipasslem11  28735  minvecolem2  28770  minvecolem3  28771  minvecolem4  28775  shsva  29215  h1datomi  29476  lnfnmuli  29939  leopsq  30024  nmopleid  30034  opsqrlem6  30040  pjnmopi  30043  hstle  30125  csmdsymi  30229  atcvatlem  30280  dpfrac1  30702  cshf1o  30770  cycpmconjslem2  30960  rspidlid  31103  elsx  31693  dya2iocnrect  31779  cvmliftphtlem  32807  satfv1  32853  satffunlem1lem2  32893  satffunlem1  32897  wlimeq12  33380  frecseq123  33393  nosupno  33503  nosupfv  33506  noinfno  33518  noinffv  33521  scutval  33589  scutun12  33599  fvray  34026  fvline  34029  tailfb  34149  uncov  35352  tan2h  35363  matunitlindflem1  35367  matunitlindflem2  35368  poimirlem32  35403  mblfinlem4  35411  mbfresfi  35417  mbfposadd  35418  itg2addnc  35425  ftc1anclem5  35448  ftc1anclem8  35451  dvasin  35455  heiborlem7  35569  igenidl  35815  el3v3  35968  atlatmstc  36929  dihglblem2N  38904  2xp3dxp2ge1d  39718  factwoffsmonot  39719  eldioph4b  40160  diophren  40162  rmxp1  40281  rmyp1  40282  rmxm1  40283  rmym1  40284  dig0  45434  i0oii  45652  onetansqsecsq  45772  cotsqcscsq  45773