Theorem mp3an2 1451

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  1458  vtoclegft  3543  tz7.7  6343  ordin  6347  onfr  6356  fprresex  8252  tfrlem11  8319  phplem2  9129  epfrs  9640  zorng  10414  tsk2  10676  tskcard  10692  gruina  10729  muladd11  11303  00id  11308  ltaddneg  11349  negsub  11429  subneg  11430  muleqadd  11781  diveq0  11806  diveq1  11826  conjmul  11858  recp1lt1  12040  nnsub  12189  addltmul  12377  nnunb  12397  zltp1le  12541  gtndiv  12569  eluzp1m1  12777  zbtwnre  12859  rebtwnz  12860  xnn0le2is012  13161  supxrbnd  13243  divelunit  13410  fznatpl1  13494  flbi2  13737  fldiv  13780  modid  13816  modm1p1mod0  13845  fzen2  13892  nn0ennn  13902  seqshft2  13951  seqf1olem1  13964  ser1const  13981  sq01  14148  expnbnd  14155  faclbnd3  14215  faclbnd5  14221  hashunsng  14315  hashunsngx  14316  hashxplem  14356  ccatrid  14511  ccats1val1  14550  ccat2s1fst  14563  sgnn  15017  01sqrexlem2  15166  01sqrexlem7  15171  leabs  15222  abs2dif  15256  cvgrat  15806  cos2t  16103  sin01gt0  16115  cos01gt0  16116  demoivre  16125  demoivreALT  16126  rpnnen2lem5  16143  rpnnen2lem12  16150  omeo  16293  gcd0id  16446  sqgcd  16489  expgcd  16490  isprm3  16610  eulerthlem2  16709  pczpre  16775  pcrec  16786  ressress  17174  mulgm1  19024  unitgrpid  20321  mdet0pr  22536  m2detleib  22575  cmpcov2  23334  ufileu  23863  tgpconncompeqg  24056  itg2ge0  25692  mdegldg  26027  abssinper  26486  ppiub  27171  chtub  27179  bposlem2  27252  lgs1  27308  cofcutr  27920  addbday  28014  negbdaylem  28052  precsexlem10  28212  oncutlt  28260  n0bday  28348  bdayn0p1  28365  eucliddivs  28372  nnzs  28382  bdaypw2n0bndlem  28459  zz12s  28471  remulscllem1  28496  colinearalglem4  28982  axsegconlem1  28990  axpaschlem  29013  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  funvtxval  29091  funiedgval  29092  vc0  30649  vcm  30651  nvmval2  30718  nvmf  30720  nvmdi  30723  nvnegneg  30724  nvpncan2  30728  nvaddsub4  30732  nvm1  30740  nvdif  30741  nvpi  30742  nvz0  30743  nvmtri  30746  nvabs  30747  nvge0  30748  imsmetlem  30765  4ipval2  30783  ipval3  30784  ipidsq  30785  dipcj  30789  sspmval  30808  ipasslem1  30906  ipasslem2  30907  dipsubdir  30923  hvsubdistr1  31124  shsubcl  31295  shsel3  31390  shunssi  31443  hosubdi  31883  lnopmi  32075  nmophmi  32106  nmopcoi  32170  opsqrlem6  32220  hstle  32305  hst0  32308  mdsl2i  32397  superpos  32429  dmdbr5ati  32497  f1rnen  32706  resvsca  33413  noinfepfnregs  35288  pthhashvtx  35322  cvmliftphtlem  35511  topdifinffinlem  37552  finixpnum  37806  tan2h  37813  poimirlem3  37824  poimirlem4  37825  poimirlem7  37828  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem24  37845  poimirlem28  37849  mblfinlem2  37859  mblfinlem4  37861  ismblfin  37862  el3v2  38427  atlatle  39580  pmaple  40021  dihglblem2N  41554  sn-ltaddneg  42709  elnnrabdioph  43049  rabren3dioph  43057  zindbi  43188  expgrowth  44576  binomcxplemnotnn0  44597  trelpss  44695  etransc  46527  mogoldbb  48031  pgrple2abl  48611  aacllem  50046