Theorem mp3an2 1445

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  mp3anl2  1452  tz7.7  6211  ordin  6215  onfr  6224  wfrlem14  7962  wfrlem17  7965  tfrlem11  8018  epfrs  9167  zorng  9920  tsk2  10181  tskcard  10197  gruina  10234  muladd11  10804  00id  10809  ltaddneg  10849  negsub  10928  subneg  10929  muleqadd  11278  diveq1  11325  conjmul  11351  recp1lt1  11532  nnsub  11675  addltmul  11867  nnunb  11887  zltp1le  12026  gtndiv  12053  eluzp1m1  12262  zbtwnre  12340  rebtwnz  12341  xnn0le2is012  12633  supxrbnd  12715  divelunit  12874  fznatpl1  12955  flbi2  13181  fldiv  13222  modid  13258  modm1p1mod0  13284  fzen2  13331  nn0ennn  13341  seqshft2  13390  seqf1olem1  13403  ser1const  13420  sq01  13580  expnbnd  13587  faclbnd3  13646  faclbnd5  13652  hashunsng  13747  hashunsngx  13748  hashxplem  13788  ccatrid  13935  ccats1val1  13975  ccat2s1fst  13994  sgnn  14447  sqrlem2  14597  sqrlem7  14602  leabs  14653  abs2dif  14686  cvgrat  15233  cos2t  15525  sin01gt0  15537  cos01gt0  15538  demoivre  15547  demoivreALT  15548  rpnnen2lem5  15565  rpnnen2lem12  15572  omeo  15709  gcd0id  15861  sqgcd  15903  isprm3  16021  eulerthlem2  16113  pczpre  16178  pcrec  16189  ressress  16556  mulgm1  18242  unitgrpid  19413  mdet0pr  21195  m2detleib  21234  cmpcov2  21992  ufileu  22521  tgpconncompeqg  22714  itg2ge0  24330  mdegldg  24654  abssinper  25100  ppiub  25774  chtub  25782  bposlem2  25855  lgs1  25911  colinearalglem4  26689  axsegconlem1  26697  axpaschlem  26720  axcontlem2  26745  axcontlem4  26747  axcontlem7  26750  axcontlem8  26751  funvtxval  26797  funiedgval  26798  vc0  28345  vcm  28347  nvmval2  28414  nvmf  28416  nvmdi  28419  nvnegneg  28420  nvpncan2  28424  nvaddsub4  28428  nvm1  28436  nvdif  28437  nvpi  28438  nvz0  28439  nvmtri  28442  nvabs  28443  nvge0  28444  imsmetlem  28461  4ipval2  28479  ipval3  28480  ipidsq  28481  dipcj  28485  sspmval  28504  ipasslem1  28602  ipasslem2  28603  dipsubdir  28619  hvsubdistr1  28820  shsubcl  28991  shsel3  29086  shunssi  29139  hosubdi  29579  lnopmi  29771  nmophmi  29802  nmopcoi  29866  opsqrlem6  29916  hstle  30001  hst0  30004  mdsl2i  30093  superpos  30125  dmdbr5ati  30193  f1rnen  30368  resvsca  30898  pthhashvtx  32369  cvmliftphtlem  32559  topdifinffinlem  34622  finixpnum  34871  tan2h  34878  poimirlem3  34889  poimirlem4  34890  poimirlem7  34893  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem20  34906  poimirlem24  34910  poimirlem28  34914  mblfinlem2  34924  mblfinlem4  34926  ismblfin  34927  el3v2  35487  atlatle  36450  pmaple  36891  dihglblem2N  38424  expgcd  39176  elnnrabdioph  39397  rabren3dioph  39405  zindbi  39536  expgrowth  40660  binomcxplemnotnn0  40681  trelpss  40780  etransc  42562  mogoldbb  43944  pgrple2abl  44407  aacllem  44896