Theorem mp3an2 1479

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3anl2  1486  vtoclegft  3547  tz7.7  6403  ordin  6408  onfr  6417  fprresex  8353  tfrlem11  8421  phplem2  9245  epfrs  9756  zorng  10606  tsk2  10874  tskcard  10890  gruina  10927  muladd11  11504  00id  11509  ltaddneg  11550  negsub  11630  subneg  11631  muleqadd  11984  diveq0  12008  diveq1  12027  conjmul  12058  recp1lt1  12239  nnsub  12406  addltmul  12606  nnunb  12626  zltp1le  12770  gtndiv  12800  eluzp1m1  13015  zbtwnre  13097  rebtwnz  13098  xnn0le2is012  13400  supxrbnd  13482  divelunit  13649  fznatpl1  13736  flbi2  13981  fldiv  14024  modid  14060  modm1p1mod0  14089  fzen2  14136  nn0ennn  14146  seqshft2  14195  seqf1olem1  14208  ser1const  14225  sq01  14393  expnbnd  14400  faclbnd3  14460  faclbnd5  14466  hashunsng  14560  hashunsngx  14561  hashxplem  14602  ccatrid  14757  ccats1val1  14799  ccat2s1fst  14812  sgnn  15273  01sqrexlem2  15436  01sqrexlem7  15441  leabs  15492  abs2dif  15526  cvgrat  16078  cos2t  16372  sin01gt0  16384  cos01gt0  16385  demoivre  16394  demoivreALT  16395  rpnnen2lem5  16412  rpnnen2lem12  16419  omeo  16562  gcd0id  16717  sqgcd  16762  expgcd  16763  isprm3  16884  eulerthlem2  16985  pczpre  17051  pcrec  17062  ressress  17451  mulgm1  19330  unitgrpid  20642  mdet0pr  22934  m2detleib  22973  cmpcov2  23735  ufileu  24265  tgpconncompeqg  24458  itg2ge0  26083  mdegldg  26411  abssinper  26876  ppiub  27558  chtub  27566  bposlem2  27639  lgs1  27695  cofcutr  28337  addbday  28431  negbdaylem  28469  precsexlem10  28629  oncutlt  28677  n0bday  28765  bdayn0p1  28782  eucliddivs  28789  nnzs  28799  bdaypw2n0bndlem  28876  zz12s  28888  remulscllem1  28913  colinearalglem4  29514  axsegconlem1  29522  axpaschlem  29545  axcontlem2  29570  axcontlem4  29572  axcontlem7  29575  axcontlem8  29576  funvtxval  29623  funiedgval  29624  pthhashvtx  30342  vc0  31203  vcm  31205  nvmval2  31272  nvmf  31274  nvmdi  31277  nvnegneg  31278  nvpncan2  31282  nvaddsub4  31286  nvm1  31294  nvdif  31295  nvpi  31296  nvz0  31297  nvmtri  31300  nvabs  31301  nvge0  31302  imsmetlem  31319  4ipval2  31337  ipval3  31338  ipidsq  31339  dipcj  31343  sspmval  31362  ipasslem1  31460  ipasslem2  31461  dipsubdir  31477  hvsubdistr1  31678  shsubcl  31849  shsel3  31944  shunssi  31997  hosubdi  32437  lnopmi  32629  nmophmi  32660  nmopcoi  32724  opsqrlem6  32774  hstle  32859  hst0  32862  mdsl2i  32951  superpos  32983  dmdbr5ati  33051  f1rnen  33291  resvsca  33960  weexenwe  35847  noinfepfnregs  35899  vonf1onprcf1ac  36043  cvmliftphtlem  36248  mh-inf3f1  37506  topdifinffinlem  38461  finixpnum  38719  tan2h  38726  poimirlem3  38732  poimirlem4  38733  poimirlem7  38736  poimirlem16  38745  poimirlem17  38746  poimirlem19  38748  poimirlem20  38749  poimirlem24  38753  poimirlem28  38757  mblfinlem2  38767  mblfinlem4  38769  ismblfin  38770  el3v2  39354  atlatle  40568  pmaple  41009  dihglblem2N  42542  sn-ltaddneg  43709  elnnrabdioph  44005  rabren3dioph  44013  zindbi  44144  expgrowth  45509  binomcxplemnotnn0  45530  trelpss  45626  etransc  47496  mogoldbb  49086  pgrple2abl  49680  aacllem  51217