Theorem mp3an2 1451

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

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

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 1091

This theorem is referenced by:  mp3anl2  1458  tz7.7  6217  ordin  6221  onfr  6230  wfrlem14  8046  wfrlem17  8049  tfrlem11  8102  epfrs  9325  zorng  10083  tsk2  10344  tskcard  10360  gruina  10397  muladd11  10967  00id  10972  ltaddneg  11012  negsub  11091  subneg  11092  muleqadd  11441  diveq1  11488  conjmul  11514  recp1lt1  11695  nnsub  11839  addltmul  12031  nnunb  12051  zltp1le  12192  gtndiv  12219  eluzp1m1  12429  zbtwnre  12507  rebtwnz  12508  xnn0le2is012  12801  supxrbnd  12883  divelunit  13047  fznatpl1  13131  flbi2  13357  fldiv  13398  modid  13434  modm1p1mod0  13460  fzen2  13507  nn0ennn  13517  seqshft2  13567  seqf1olem1  13580  ser1const  13597  sq01  13757  expnbnd  13764  faclbnd3  13823  faclbnd5  13829  hashunsng  13924  hashunsngx  13925  hashxplem  13965  ccatrid  14109  ccats1val1  14149  ccat2s1fst  14168  sgnn  14622  sqrlem2  14772  sqrlem7  14777  leabs  14828  abs2dif  14861  cvgrat  15410  cos2t  15702  sin01gt0  15714  cos01gt0  15715  demoivre  15724  demoivreALT  15725  rpnnen2lem5  15742  rpnnen2lem12  15749  omeo  15890  gcd0id  16041  sqgcd  16085  isprm3  16203  eulerthlem2  16298  pczpre  16363  pcrec  16374  ressress  16746  mulgm1  18466  unitgrpid  19641  mdet0pr  21443  m2detleib  21482  cmpcov2  22241  ufileu  22770  tgpconncompeqg  22963  itg2ge0  24587  mdegldg  24918  abssinper  25364  ppiub  26039  chtub  26047  bposlem2  26120  lgs1  26176  colinearalglem4  26954  axsegconlem1  26962  axpaschlem  26985  axcontlem2  27010  axcontlem4  27012  axcontlem7  27015  axcontlem8  27016  funvtxval  27063  funiedgval  27064  vc0  28609  vcm  28611  nvmval2  28678  nvmf  28680  nvmdi  28683  nvnegneg  28684  nvpncan2  28688  nvaddsub4  28692  nvm1  28700  nvdif  28701  nvpi  28702  nvz0  28703  nvmtri  28706  nvabs  28707  nvge0  28708  imsmetlem  28725  4ipval2  28743  ipval3  28744  ipidsq  28745  dipcj  28749  sspmval  28768  ipasslem1  28866  ipasslem2  28867  dipsubdir  28883  hvsubdistr1  29084  shsubcl  29255  shsel3  29350  shunssi  29403  hosubdi  29843  lnopmi  30035  nmophmi  30066  nmopcoi  30130  opsqrlem6  30180  hstle  30265  hst0  30268  mdsl2i  30357  superpos  30389  dmdbr5ati  30457  f1rnen  30637  resvsca  31202  pthhashvtx  32756  cvmliftphtlem  32946  cofcutr  33778  topdifinffinlem  35204  finixpnum  35448  tan2h  35455  poimirlem3  35466  poimirlem4  35467  poimirlem7  35470  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem24  35487  poimirlem28  35491  mblfinlem2  35501  mblfinlem4  35503  ismblfin  35504  el3v2  36059  atlatle  37020  pmaple  37461  dihglblem2N  38994  expgcd  39983  elnnrabdioph  40273  rabren3dioph  40281  zindbi  40412  expgrowth  41567  binomcxplemnotnn0  41588  trelpss  41687  etransc  43442  mogoldbb  44853  pgrple2abl  45317  aacllem  46119