Theorem mp3an2 1450

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

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

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 1088

This theorem is referenced by:  mp3anl2  1457  vtoclegft  3587  tz7.7  6409  ordin  6413  onfr  6422  fprresex  8336  wfrlem14OLD  8363  wfrlem17OLD  8366  tfrlem11  8429  phplem2  9246  epfrs  9772  zorng  10545  tsk2  10806  tskcard  10822  gruina  10859  muladd11  11432  00id  11437  ltaddneg  11478  negsub  11558  subneg  11559  muleqadd  11908  diveq0  11933  diveq1  11953  conjmul  11985  recp1lt1  12167  nnsub  12311  addltmul  12504  nnunb  12524  zltp1le  12669  gtndiv  12697  eluzp1m1  12905  zbtwnre  12989  rebtwnz  12990  xnn0le2is012  13289  supxrbnd  13371  divelunit  13535  fznatpl1  13619  flbi2  13858  fldiv  13901  modid  13937  modm1p1mod0  13964  fzen2  14011  nn0ennn  14021  seqshft2  14070  seqf1olem1  14083  ser1const  14100  sq01  14265  expnbnd  14272  faclbnd3  14332  faclbnd5  14338  hashunsng  14432  hashunsngx  14433  hashxplem  14473  ccatrid  14626  ccats1val1  14665  ccat2s1fst  14678  sgnn  15134  01sqrexlem2  15283  01sqrexlem7  15288  leabs  15339  abs2dif  15372  cvgrat  15920  cos2t  16215  sin01gt0  16227  cos01gt0  16228  demoivre  16237  demoivreALT  16238  rpnnen2lem5  16255  rpnnen2lem12  16262  omeo  16404  gcd0id  16557  sqgcd  16600  expgcd  16601  isprm3  16721  eulerthlem2  16820  pczpre  16886  pcrec  16897  ressress  17294  mulgm1  19113  unitgrpid  20386  mdet0pr  22599  m2detleib  22638  cmpcov2  23399  ufileu  23928  tgpconncompeqg  24121  itg2ge0  25771  mdegldg  26106  abssinper  26564  ppiub  27249  chtub  27257  bposlem2  27330  lgs1  27386  cofcutr  27959  addsbday  28051  negsbdaylem  28089  precsexlem10  28241  n0sbday  28355  nnzs  28373  pw2bday  28419  zzs12  28424  remulscllem1  28433  colinearalglem4  28925  axsegconlem1  28933  axpaschlem  28956  axcontlem2  28981  axcontlem4  28983  axcontlem7  28986  axcontlem8  28987  funvtxval  29036  funiedgval  29037  vc0  30594  vcm  30596  nvmval2  30663  nvmf  30665  nvmdi  30668  nvnegneg  30669  nvpncan2  30673  nvaddsub4  30677  nvm1  30685  nvdif  30686  nvpi  30687  nvz0  30688  nvmtri  30691  nvabs  30692  nvge0  30693  imsmetlem  30710  4ipval2  30728  ipval3  30729  ipidsq  30730  dipcj  30734  sspmval  30753  ipasslem1  30851  ipasslem2  30852  dipsubdir  30868  hvsubdistr1  31069  shsubcl  31240  shsel3  31335  shunssi  31388  hosubdi  31828  lnopmi  32020  nmophmi  32051  nmopcoi  32115  opsqrlem6  32165  hstle  32250  hst0  32253  mdsl2i  32342  superpos  32374  dmdbr5ati  32442  f1rnen  32640  resvsca  33357  pthhashvtx  35134  cvmliftphtlem  35323  topdifinffinlem  37349  finixpnum  37613  tan2h  37620  poimirlem3  37631  poimirlem4  37632  poimirlem7  37635  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem24  37652  poimirlem28  37656  mblfinlem2  37666  mblfinlem4  37668  ismblfin  37669  el3v2  38227  atlatle  39322  pmaple  39764  dihglblem2N  41297  sn-ltaddneg  42477  elnnrabdioph  42823  rabren3dioph  42831  zindbi  42963  expgrowth  44359  binomcxplemnotnn0  44380  trelpss  44479  etransc  46303  mogoldbb  47777  pgrple2abl  48286  aacllem  49375