Theorem mp3an2 1452

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 702	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mp3anl2  1459  vtoclegft  3529  tz7.7  6338  ordin  6342  onfr  6351  fprresex  8249  tfrlem11  8316  phplem2  9128  epfrs  9641  zorng  10415  tsk2  10677  tskcard  10693  gruina  10730  muladd11  11305  00id  11310  ltaddneg  11351  negsub  11431  subneg  11432  muleqadd  11783  diveq0  11808  diveq1  11828  conjmul  11861  recp1lt1  12043  nnsub  12210  addltmul  12402  nnunb  12422  zltp1le  12566  gtndiv  12595  eluzp1m1  12803  zbtwnre  12885  rebtwnz  12886  xnn0le2is012  13187  supxrbnd  13269  divelunit  13436  fznatpl1  13521  flbi2  13765  fldiv  13808  modid  13844  modm1p1mod0  13873  fzen2  13920  nn0ennn  13930  seqshft2  13979  seqf1olem1  13992  ser1const  14009  sq01  14176  expnbnd  14183  faclbnd3  14243  faclbnd5  14249  hashunsng  14343  hashunsngx  14344  hashxplem  14384  ccatrid  14539  ccats1val1  14578  ccat2s1fst  14591  sgnn  15045  01sqrexlem2  15194  01sqrexlem7  15199  leabs  15250  abs2dif  15284  cvgrat  15837  cos2t  16134  sin01gt0  16146  cos01gt0  16147  demoivre  16156  demoivreALT  16157  rpnnen2lem5  16174  rpnnen2lem12  16181  omeo  16324  gcd0id  16477  sqgcd  16520  expgcd  16521  isprm3  16641  eulerthlem2  16741  pczpre  16807  pcrec  16818  ressress  17206  mulgm1  19059  unitgrpid  20354  mdet0pr  22545  m2detleib  22584  cmpcov2  23343  ufileu  23872  tgpconncompeqg  24065  itg2ge0  25690  mdegldg  26019  abssinper  26473  ppiub  27155  chtub  27163  bposlem2  27236  lgs1  27292  cofcutr  27904  addbday  27998  negbdaylem  28036  precsexlem10  28196  oncutlt  28244  n0bday  28332  bdayn0p1  28349  eucliddivs  28356  nnzs  28366  bdaypw2n0bndlem  28443  zz12s  28455  remulscllem1  28480  colinearalglem4  28966  axsegconlem1  28974  axpaschlem  28997  axcontlem2  29022  axcontlem4  29024  axcontlem7  29027  axcontlem8  29028  funvtxval  29075  funiedgval  29076  vc0  30633  vcm  30635  nvmval2  30702  nvmf  30704  nvmdi  30707  nvnegneg  30708  nvpncan2  30712  nvaddsub4  30716  nvm1  30724  nvdif  30725  nvpi  30726  nvz0  30727  nvmtri  30730  nvabs  30731  nvge0  30732  imsmetlem  30749  4ipval2  30767  ipval3  30768  ipidsq  30769  dipcj  30773  sspmval  30792  ipasslem1  30890  ipasslem2  30891  dipsubdir  30907  hvsubdistr1  31108  shsubcl  31279  shsel3  31374  shunssi  31427  hosubdi  31867  lnopmi  32059  nmophmi  32090  nmopcoi  32154  opsqrlem6  32204  hstle  32289  hst0  32292  mdsl2i  32381  superpos  32413  dmdbr5ati  32481  f1rnen  32689  resvsca  33380  noinfepfnregs  35264  pthhashvtx  35298  cvmliftphtlem  35487  topdifinffinlem  37651  finixpnum  37914  tan2h  37921  poimirlem3  37932  poimirlem4  37933  poimirlem7  37936  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem24  37953  poimirlem28  37957  mblfinlem2  37967  mblfinlem4  37969  ismblfin  37970  el3v2  38540  atlatle  39754  pmaple  40195  dihglblem2N  41728  sn-ltaddneg  42887  elnnrabdioph  43223  rabren3dioph  43231  zindbi  43362  expgrowth  44750  binomcxplemnotnn0  44771  trelpss  44869  etransc  46699  mogoldbb  48249  pgrple2abl  48829  aacllem  50264