Theorem mp3an2 1450

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an2.1	⊢ 𝜓
mp3an2.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1119	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 700	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  mp3anl2  1457  vtoclegft  3574  tz7.7  6391  ordin  6395  onfr  6404  fprresex  8295  wfrlem14OLD  8322  wfrlem17OLD  8325  tfrlem11  8388  phplem2  9208  epfrs  9726  zorng  10499  tsk2  10760  tskcard  10776  gruina  10813  muladd11  11384  00id  11389  ltaddneg  11429  negsub  11508  subneg  11509  muleqadd  11858  diveq1  11905  conjmul  11931  recp1lt1  12112  nnsub  12256  addltmul  12448  nnunb  12468  zltp1le  12612  gtndiv  12639  eluzp1m1  12848  zbtwnre  12930  rebtwnz  12931  xnn0le2is012  13225  supxrbnd  13307  divelunit  13471  fznatpl1  13555  flbi2  13782  fldiv  13825  modid  13861  modm1p1mod0  13887  fzen2  13934  nn0ennn  13944  seqshft2  13994  seqf1olem1  14007  ser1const  14024  sq01  14188  expnbnd  14195  faclbnd3  14252  faclbnd5  14258  hashunsng  14352  hashunsngx  14353  hashxplem  14393  ccatrid  14537  ccats1val1  14576  ccat2s1fst  14589  sgnn  15041  01sqrexlem2  15190  01sqrexlem7  15195  leabs  15246  abs2dif  15279  cvgrat  15829  cos2t  16121  sin01gt0  16133  cos01gt0  16134  demoivre  16143  demoivreALT  16144  rpnnen2lem5  16161  rpnnen2lem12  16168  omeo  16309  gcd0id  16460  sqgcd  16502  isprm3  16620  eulerthlem2  16715  pczpre  16780  pcrec  16791  ressress  17193  mulgm1  18974  unitgrpid  20199  mdet0pr  22094  m2detleib  22133  cmpcov2  22894  ufileu  23423  tgpconncompeqg  23616  itg2ge0  25253  mdegldg  25584  abssinper  26030  ppiub  26707  chtub  26715  bposlem2  26788  lgs1  26844  cofcutr  27413  negsbdaylem  27533  precsexlem10  27665  colinearalglem4  28198  axsegconlem1  28206  axpaschlem  28229  axcontlem2  28254  axcontlem4  28256  axcontlem7  28259  axcontlem8  28260  funvtxval  28309  funiedgval  28310  vc0  29858  vcm  29860  nvmval2  29927  nvmf  29929  nvmdi  29932  nvnegneg  29933  nvpncan2  29937  nvaddsub4  29941  nvm1  29949  nvdif  29950  nvpi  29951  nvz0  29952  nvmtri  29955  nvabs  29956  nvge0  29957  imsmetlem  29974  4ipval2  29992  ipval3  29993  ipidsq  29994  dipcj  29998  sspmval  30017  ipasslem1  30115  ipasslem2  30116  dipsubdir  30132  hvsubdistr1  30333  shsubcl  30504  shsel3  30599  shunssi  30652  hosubdi  31092  lnopmi  31284  nmophmi  31315  nmopcoi  31379  opsqrlem6  31429  hstle  31514  hst0  31517  mdsl2i  31606  superpos  31638  dmdbr5ati  31706  f1rnen  31884  resvsca  32475  pthhashvtx  34149  cvmliftphtlem  34339  topdifinffinlem  36276  finixpnum  36521  tan2h  36528  poimirlem3  36539  poimirlem4  36540  poimirlem7  36543  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem24  36560  poimirlem28  36564  mblfinlem2  36574  mblfinlem4  36576  ismblfin  36577  el3v2  37136  atlatle  38238  pmaple  38680  dihglblem2N  40213  expgcd  41273  sn-ltaddneg  41363  elnnrabdioph  41593  rabren3dioph  41601  zindbi  41733  expgrowth  43142  binomcxplemnotnn0  43163  trelpss  43262  etransc  45047  mogoldbb  46501  pgrple2abl  47089  aacllem  47896