Theorem mp3an3 1411

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  mp3an13  1413  mp3an23  1414  mp3anl3  1418  opelxp  5136  ov  6765  ovmpt2a  6776  ovmpt2  6781  oaword1  7617  oneo  7646  oeoalem  7661  oeoelem  7663  nnaword1  7694  nnneo  7716  erov  7829  enrefg  7972  f1imaen  8003  mapxpen  8111  acnlem  8856  cdacomen  8988  infmap  9383  canthnumlem  9455  tskin  9566  tsksn  9567  tsk0  9570  gruxp  9614  gruina  9625  genpprecl  9808  addsrpr  9881  mulsrpr  9882  supsrlem  9917  mulid1  10022  00id  10196  mul02lem1  10197  ltneg  10513  leneg  10516  suble0  10527  div1  10701  nnaddcl  11027  nnmulcl  11028  nnge1  11031  nnsub  11044  2halves  11245  halfaddsub  11250  addltmul  11253  zleltp1  11413  nnaddm1cl  11419  zextlt  11436  eluzp1p1  11698  uzaddcl  11729  znq  11777  xrre  11985  xrre2  11986  fzshftral  12412  fraclt1  12586  expadd  12885  expmul  12888  expubnd  12904  sqmul  12909  bernneq  12973  faclbnd2  13061  faclbnd6  13069  hashgadd  13149  hashun2  13155  hashssdif  13183  hashfun  13207  ccatlcan  13454  ccatrcan  13455  shftval3  13797  sqrlem1  13964  caubnd2  14078  bpoly2  14769  bpoly3  14770  fsumcube  14772  efexp  14812  efival  14863  cos01gt0  14902  odd2np1  15046  halfleoddlt  15067  omoe  15069  opeo  15070  divalglem5  15101  gcdmultiple  15250  sqgcd  15259  nn0seqcvgd  15264  phiprmpw  15462  eulerthlem2  15468  odzcllem  15478  pythagtriplem15  15515  pythagtriplem17  15517  pcelnn  15555  4sqlem3  15635  xpscfn  16200  fullfunc  16547  fthfunc  16548  prfcl  16824  curf1cl  16849  curfcl  16853  hofcl  16880  odinv  17959  lsmelvalix  18037  dprdval  18383  lsp0  18990  lss0v  18997  coe1scl  19638  zndvds0  19880  frlmlbs  20117  lindfres  20143  lmisfree  20162  ntrin  20846  lpsscls  20926  restperf  20969  txuni2  21349  txopn  21386  elqtop2  21485  xkocnv  21598  ptcmp  21843  xblpnfps  22181  xblpnf  22182  bl2in  22186  unirnblps  22205  unirnbl  22206  blpnfctr  22222  dscopn  22359  bcthlem4  23105  minveclem2  23178  minveclem4  23184  icombl  23313  i1fadd  23443  i1fmul  23444  dvn1  23670  dvexp3  23722  plyconst  23943  plyid  23946  sincosq1eq  24245  sinord  24261  cxpp1  24407  cxpsqrtlem  24429  cxpsqrt  24430  angneg  24514  dcubic  24554  issqf  24843  ppiub  24910  bposlem1  24990  bposlem2  24991  bposlem9  24998  axlowdimlem6  25808  axlowdimlem14  25816  axcontlem2  25826  structgrssvtxlemOLD  25896  pthdlem2  26645  0ewlk  26955  ipasslem1  27656  ipasslem2  27657  ipasslem11  27665  minvecolem2  27701  minvecolem3  27702  minvecolem4  27706  shsva  28149  h1datomi  28410  lnfnmuli  28873  leopsq  28958  nmopleid  28968  opsqrlem6  28974  pjnmopi  28977  hstle  29059  csmdsymi  29163  atcvatlem  29214  dpfrac1  29573  dpfrac1OLD  29574  elsx  30231  dya2iocnrect  30317  cvmliftphtlem  31273  wlimeq12  31739  nosupno  31823  nosupfv  31826  scutval  31885  scutun12  31891  fvray  32223  fvline  32226  tailfb  32347  uncov  33361  tan2h  33372  matunitlindflem1  33376  matunitlindflem2  33377  poimirlem32  33412  mblfinlem4  33420  mbfresfi  33427  mbfposadd  33428  itg2addnc  33435  ftc1anclem5  33460  ftc1anclem8  33463  dvasin  33467  heiborlem7  33587  igenidl  33833  atlatmstc  34425  dihglblem2N  36402  eldioph4b  37194  diophren  37196  rmxp1  37316  rmyp1  37317  rmxm1  37318  rmym1  37319  wepwso  37432  pfx2  41177  dig0  42165  onetansqsecsq  42267  cotsqcscsq  42268