Theorem mp3an2 1412

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  mp3anl2  1419  tz7.7  5749  ordin  5753  onfr  5763  wfrlem14  7428  wfrlem17  7431  tfrlem11  7484  epfrs  8607  zorng  9326  tsk2  9587  tskcard  9603  gruina  9640  muladd11  10206  00id  10211  ltaddneg  10251  negsub  10329  subneg  10330  muleqadd  10671  diveq1  10718  conjmul  10742  recp1lt1  10921  nnsub  11059  addltmul  11268  nnunb  11288  zltp1le  11427  gtndiv  11454  eluzp1m1  11711  zbtwnre  11786  rebtwnz  11787  xnn0le2is012  12076  supxrbnd  12158  divelunit  12314  fznatpl1  12395  flbi2  12618  fldiv  12659  modid  12695  modm1p1mod0  12721  fzen2  12768  nn0ennn  12778  seqshft2  12827  seqf1olem1  12840  ser1const  12857  sq01  12986  expnbnd  12993  faclbnd3  13079  faclbnd5  13085  hashunsng  13181  hashxplem  13220  ccatrid  13370  sgnn  13834  sqrlem2  13984  sqrlem7  13989  leabs  14039  abs2dif  14072  cvgrat  14615  cos2t  14908  sin01gt0  14920  cos01gt0  14921  demoivre  14930  demoivreALT  14931  znnenlem  14940  rpnnen2lem5  14947  rpnnen2lem12  14954  omeo  15090  gcd0id  15240  sqgcd  15278  isprm3  15396  eulerthlem2  15487  pczpre  15552  pcrec  15563  ressress  15938  mulgm1  17562  unitgrpid  18669  mdet0pr  20398  m2detleib  20437  cmpcov2  21193  ufileu  21723  tgpconncompeqg  21915  itg2ge0  23502  mdegldg  23826  abssinper  24270  ppiub  24929  chtub  24937  bposlem2  25010  lgs1  25066  colinearalglem4  25789  axsegconlem1  25797  axpaschlem  25820  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  funvtxval  25905  funiedgval  25906  vc0  27429  vcm  27431  nvmval2  27498  nvmf  27500  nvmdi  27503  nvnegneg  27504  nvpncan2  27508  nvaddsub4  27512  nvm1  27520  nvdif  27521  nvpi  27522  nvz0  27523  nvmtri  27526  nvabs  27527  nvge0  27528  imsmetlem  27545  4ipval2  27563  ipval3  27564  ipidsq  27565  dipcj  27569  sspmval  27588  ipasslem1  27686  ipasslem2  27687  dipsubdir  27703  hvsubdistr1  27906  shsubcl  28077  shsel3  28174  shunssi  28227  hosubdi  28667  lnopmi  28859  nmophmi  28890  nmopcoi  28954  opsqrlem6  29004  hstle  29089  hst0  29092  mdsl2i  29181  superpos  29213  dmdbr5ati  29281  resvsca  29830  cvmliftphtlem  31299  topdifinffinlem  33195  finixpnum  33394  tan2h  33401  poimirlem3  33412  poimirlem4  33413  poimirlem7  33416  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem24  33433  poimirlem28  33437  mblfinlem2  33447  mblfinlem4  33449  ismblfin  33450  el3v2  33989  atlatle  34607  pmaple  35047  dihglblem2N  36583  elnnrabdioph  37371  rabren3dioph  37379  zindbi  37511  expgrowth  38534  binomcxplemnotnn0  38555  trelpss  38659  etransc  40500  mogoldbb  41673  pgrple2abl  42146  aacllem  42547