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  3532  tz7.7  6347  ordin  6351  onfr  6360  fprresex  8257  tfrlem11  8324  phplem2  9136  epfrs  9649  zorng  10423  tsk2  10685  tskcard  10701  gruina  10738  muladd11  11313  00id  11318  ltaddneg  11359  negsub  11439  subneg  11440  muleqadd  11791  diveq0  11816  diveq1  11836  conjmul  11869  recp1lt1  12051  nnsub  12218  addltmul  12410  nnunb  12430  zltp1le  12574  gtndiv  12603  eluzp1m1  12811  zbtwnre  12893  rebtwnz  12894  xnn0le2is012  13195  supxrbnd  13277  divelunit  13444  fznatpl1  13529  flbi2  13773  fldiv  13816  modid  13852  modm1p1mod0  13881  fzen2  13928  nn0ennn  13938  seqshft2  13987  seqf1olem1  14000  ser1const  14017  sq01  14184  expnbnd  14191  faclbnd3  14251  faclbnd5  14257  hashunsng  14351  hashunsngx  14352  hashxplem  14392  ccatrid  14547  ccats1val1  14586  ccat2s1fst  14599  sgnn  15053  01sqrexlem2  15202  01sqrexlem7  15207  leabs  15258  abs2dif  15292  cvgrat  15845  cos2t  16142  sin01gt0  16154  cos01gt0  16155  demoivre  16164  demoivreALT  16165  rpnnen2lem5  16182  rpnnen2lem12  16189  omeo  16332  gcd0id  16485  sqgcd  16528  expgcd  16529  isprm3  16649  eulerthlem2  16749  pczpre  16815  pcrec  16826  ressress  17214  mulgm1  19067  unitgrpid  20362  mdet0pr  22573  m2detleib  22612  cmpcov2  23371  ufileu  23900  tgpconncompeqg  24093  itg2ge0  25718  mdegldg  26047  abssinper  26504  ppiub  27187  chtub  27195  bposlem2  27268  lgs1  27324  cofcutr  27936  addbday  28030  negbdaylem  28068  precsexlem10  28228  oncutlt  28276  n0bday  28364  bdayn0p1  28381  eucliddivs  28388  nnzs  28398  bdaypw2n0bndlem  28475  zz12s  28487  remulscllem1  28512  colinearalglem4  28998  axsegconlem1  29006  axpaschlem  29029  axcontlem2  29054  axcontlem4  29056  axcontlem7  29059  axcontlem8  29060  funvtxval  29107  funiedgval  29108  vc0  30666  vcm  30668  nvmval2  30735  nvmf  30737  nvmdi  30740  nvnegneg  30741  nvpncan2  30745  nvaddsub4  30749  nvm1  30757  nvdif  30758  nvpi  30759  nvz0  30760  nvmtri  30763  nvabs  30764  nvge0  30765  imsmetlem  30782  4ipval2  30800  ipval3  30801  ipidsq  30802  dipcj  30806  sspmval  30825  ipasslem1  30923  ipasslem2  30924  dipsubdir  30940  hvsubdistr1  31141  shsubcl  31312  shsel3  31407  shunssi  31460  hosubdi  31900  lnopmi  32092  nmophmi  32123  nmopcoi  32187  opsqrlem6  32237  hstle  32322  hst0  32325  mdsl2i  32414  superpos  32446  dmdbr5ati  32514  f1rnen  32722  resvsca  33413  noinfepfnregs  35298  pthhashvtx  35332  cvmliftphtlem  35521  topdifinffinlem  37685  finixpnum  37948  tan2h  37955  poimirlem3  37966  poimirlem4  37967  poimirlem7  37970  poimirlem16  37979  poimirlem17  37980  poimirlem19  37982  poimirlem20  37983  poimirlem24  37987  poimirlem28  37991  mblfinlem2  38001  mblfinlem4  38003  ismblfin  38004  el3v2  38574  atlatle  39788  pmaple  40229  dihglblem2N  41762  sn-ltaddneg  42921  elnnrabdioph  43261  rabren3dioph  43269  zindbi  43400  expgrowth  44788  binomcxplemnotnn0  44809  trelpss  44907  etransc  46737  mogoldbb  48281  pgrple2abl  48861  aacllem  50296