Theorem mp3an2 1404

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 1257	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 713	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  mp3anl2  1411  tz7.7  5666  ordin  5670  onfr  5680  wfrlem14  7315  wfrlem17  7318  tfrlem11  7371  epfrs  8490  zorng  9209  tsk2  9466  tskcard  9482  gruina  9519  muladd11  10085  00id  10090  ltaddneg  10130  negsub  10208  subneg  10209  muleqadd  10550  diveq1  10597  conjmul  10621  recp1lt1  10800  nnsub  10936  addltmul  11145  nnunb  11165  zltp1le  11304  gtndiv  11330  eluzp1m1  11587  zbtwnre  11662  rebtwnz  11663  supxrbnd  12030  divelunit  12185  fznatpl1  12265  flbi2  12480  fldiv  12521  modid  12557  modm1p1mod0  12583  fzen2  12630  nn0ennn  12640  seqshft2  12689  seqf1olem1  12702  ser1const  12719  sq01  12848  expnbnd  12855  faclbnd3  12941  faclbnd5  12947  hashunsng  13042  hashxplem  13080  ccatrid  13223  sgnn  13682  sqrlem2  13832  sqrlem7  13837  leabs  13887  abs2dif  13920  cvgrat  14454  cos2t  14747  sin01gt0  14759  cos01gt0  14760  demoivre  14769  demoivreALT  14770  znnenlem  14779  rpnnen2lem5  14786  rpnnen2lem12  14793  omeo  14928  gcd0id  15078  sqgcd  15116  isprm3  15234  eulerthlem2  15325  pczpre  15390  pcrec  15401  ressress  15765  mulgm1  17385  unitgrpid  18492  mdet0pr  20217  m2detleib  20256  cmpcov2  21003  ufileu  21533  tgpconcompeqg  21725  itg2ge0  23308  mdegldg  23630  abssinper  24074  ppiub  24729  chtub  24737  bposlem2  24810  lgs1  24866  colinearalglem4  25589  axsegconlem1  25597  axpaschlem  25620  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem8  25651  upgredg  25811  constr2spthlem1  26124  2pthon3v  26134  el2spthonot  26397  el2spthonot0  26398  frg2woteq  26587  vc0  26813  vcm  26815  nvmval2  26882  nvmf  26884  nvmdi  26887  nvnegneg  26888  nvpncan2  26892  nvaddsub4  26896  nvm1  26904  nvdif  26905  nvpi  26906  nvz0  26907  nvmtri  26910  nvabs  26911  nvge0  26912  imsmetlem  26929  4ipval2  26947  ipval3  26948  ipidsq  26949  dipcj  26953  sspmval  26972  ipasslem1  27070  ipasslem2  27071  dipsubdir  27087  hvsubdistr1  27290  shsubcl  27461  shsel3  27558  shunssi  27611  hosubdi  28051  lnopmi  28243  nmophmi  28274  nmopcoi  28338  opsqrlem6  28388  hstle  28473  hst0  28476  mdsl2i  28565  superpos  28597  dmdbr5ati  28665  resvsca  29161  cvmliftphtlem  30553  topdifinffinlem  32371  finixpnum  32564  tan2h  32571  poimirlem3  32582  poimirlem4  32583  poimirlem7  32586  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem24  32603  poimirlem28  32607  mblfinlem2  32617  mblfinlem4  32619  ismblfin  32620  atlatle  33625  pmaple  34065  dihglblem2N  35601  elnnrabdioph  36389  rabren3dioph  36397  zindbi  36529  expgrowth  37556  binomcxplemnotnn0  37577  trelpss  37680  etransc  39176  01wlk  41284  0Trl  41290  0pth-av  41293  0spth-av  41294  0Crct  41300  0Cycl  41301  pgrple2abl  41940  aacllem  42356