Theorem mp3an2 1476

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3anl2  1483  vtoclegft  3547  tz7.7  6386  ordin  6391  onfr  6400  fprresex  8306  tfrlem11  8374  phplem2  9188  epfrs  9699  zorng  10487  tsk2  10749  tskcard  10765  gruina  10802  muladd11  11379  00id  11384  ltaddneg  11425  negsub  11505  subneg  11506  muleqadd  11857  diveq0  11881  diveq1  11900  conjmul  11931  recp1lt1  12112  nnsub  12279  addltmul  12479  nnunb  12499  zltp1le  12643  gtndiv  12672  eluzp1m1  12887  zbtwnre  12969  rebtwnz  12970  xnn0le2is012  13271  supxrbnd  13353  divelunit  13520  fznatpl1  13605  flbi2  13849  fldiv  13892  modid  13928  modm1p1mod0  13957  fzen2  14004  nn0ennn  14014  seqshft2  14063  seqf1olem1  14076  ser1const  14093  sq01  14260  expnbnd  14267  faclbnd3  14327  faclbnd5  14333  hashunsng  14427  hashunsngx  14428  hashxplem  14469  ccatrid  14624  ccats1val1  14663  ccat2s1fst  14676  sgnn  15130  01sqrexlem2  15293  01sqrexlem7  15298  leabs  15349  abs2dif  15383  cvgrat  15936  cos2t  16233  sin01gt0  16245  cos01gt0  16246  demoivre  16255  demoivreALT  16256  rpnnen2lem5  16273  rpnnen2lem12  16280  omeo  16423  gcd0id  16576  sqgcd  16619  expgcd  16620  isprm3  16740  eulerthlem2  16840  pczpre  16906  pcrec  16917  ressress  17306  mulgm1  19159  unitgrpid  20466  mdet0pr  22728  m2detleib  22767  cmpcov2  23526  ufileu  24055  tgpconncompeqg  24248  itg2ge0  25873  mdegldg  26202  abssinper  26662  ppiub  27344  chtub  27352  bposlem2  27425  lgs1  27481  cofcutr  28093  addbday  28187  negbdaylem  28225  precsexlem10  28385  oncutlt  28433  n0bday  28521  bdayn0p1  28538  eucliddivs  28545  nnzs  28555  bdaypw2n0bndlem  28632  zz12s  28644  remulscllem1  28669  colinearalglem4  29225  axsegconlem1  29233  axpaschlem  29256  axcontlem2  29281  axcontlem4  29283  axcontlem7  29286  axcontlem8  29287  funvtxval  29334  funiedgval  29335  vc0  30892  vcm  30894  nvmval2  30961  nvmf  30963  nvmdi  30966  nvnegneg  30967  nvpncan2  30971  nvaddsub4  30975  nvm1  30983  nvdif  30984  nvpi  30985  nvz0  30986  nvmtri  30989  nvabs  30990  nvge0  30991  imsmetlem  31008  4ipval2  31026  ipval3  31027  ipidsq  31028  dipcj  31032  sspmval  31051  ipasslem1  31149  ipasslem2  31150  dipsubdir  31166  hvsubdistr1  31367  shsubcl  31538  shsel3  31633  shunssi  31686  hosubdi  32126  lnopmi  32318  nmophmi  32349  nmopcoi  32413  opsqrlem6  32463  hstle  32548  hst0  32551  mdsl2i  32640  superpos  32672  dmdbr5ati  32740  f1rnen  32939  resvsca  33618  noinfepfnregs  35499  pthhashvtx  35574  cvmliftphtlem  35763  topdifinffinlem  37937  finixpnum  38200  tan2h  38207  poimirlem3  38218  poimirlem4  38219  poimirlem7  38222  poimirlem16  38231  poimirlem17  38232  poimirlem19  38234  poimirlem20  38235  poimirlem24  38239  poimirlem28  38243  mblfinlem2  38253  mblfinlem4  38255  ismblfin  38256  el3v2  38826  atlatle  40040  pmaple  40481  dihglblem2N  42014  sn-ltaddneg  43174  elnnrabdioph  43482  rabren3dioph  43490  zindbi  43621  expgrowth  44993  binomcxplemnotnn0  45014  trelpss  45111  etransc  46945  mogoldbb  48495  pgrple2abl  49090  aacllem  50546