Theorem mp3an2 1428

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

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  mp3anl2  1435  tz7.7  6052  ordin  6056  onfr  6065  wfrlem14  7770  wfrlem17  7773  tfrlem11  7826  epfrs  8965  zorng  9722  tsk2  9983  tskcard  9999  gruina  10036  muladd11  10608  00id  10613  ltaddneg  10653  negsub  10733  subneg  10734  muleqadd  11083  diveq1  11130  conjmul  11156  recp1lt1  11337  nnsub  11482  addltmul  11681  nnunb  11701  zltp1le  11843  gtndiv  11870  eluzp1m1  12080  zbtwnre  12158  rebtwnz  12159  xnn0le2is012  12453  supxrbnd  12535  divelunit  12694  fznatpl1  12775  flbi2  13000  fldiv  13041  modid  13077  modm1p1mod0  13103  fzen2  13150  nn0ennn  13160  seqshft2  13209  seqf1olem1  13222  ser1const  13239  sq01  13399  expnbnd  13406  faclbnd3  13465  faclbnd5  13471  hashunsng  13564  hashunsngx  13565  hashxplem  13605  ccatrid  13748  sgnn  14312  sqrlem2  14462  sqrlem7  14467  leabs  14518  abs2dif  14551  cvgrat  15097  cos2t  15389  sin01gt0  15401  cos01gt0  15402  demoivre  15411  demoivreALT  15412  rpnnen2lem5  15429  rpnnen2lem12  15436  omeo  15573  gcd0id  15725  sqgcd  15763  isprm3  15881  eulerthlem2  15973  pczpre  16038  pcrec  16049  ressress  16416  mulgm1  18045  unitgrpid  19154  mdet0pr  20917  m2detleib  20956  cmpcov2  21714  ufileu  22243  tgpconncompeqg  22435  itg2ge0  24051  mdegldg  24375  abssinper  24821  ppiub  25494  chtub  25502  bposlem2  25575  lgs1  25631  colinearalglem4  26410  axsegconlem1  26418  axpaschlem  26441  axcontlem2  26466  axcontlem4  26468  axcontlem7  26471  axcontlem8  26472  funvtxval  26518  funiedgval  26519  vc0  28140  vcm  28142  nvmval2  28209  nvmf  28211  nvmdi  28214  nvnegneg  28215  nvpncan2  28219  nvaddsub4  28223  nvm1  28231  nvdif  28232  nvpi  28233  nvz0  28234  nvmtri  28237  nvabs  28238  nvge0  28239  imsmetlem  28256  4ipval2  28274  ipval3  28275  ipidsq  28276  dipcj  28280  sspmval  28299  ipasslem1  28397  ipasslem2  28398  dipsubdir  28414  hvsubdistr1  28617  shsubcl  28788  shsel3  28885  shunssi  28938  hosubdi  29378  lnopmi  29570  nmophmi  29601  nmopcoi  29665  opsqrlem6  29715  hstle  29800  hst0  29803  mdsl2i  29892  superpos  29924  dmdbr5ati  29992  f1rnen  30151  resvsca  30611  cvmliftphtlem  32178  topdifinffinlem  34099  finixpnum  34347  tan2h  34354  poimirlem3  34365  poimirlem4  34366  poimirlem7  34369  poimirlem16  34378  poimirlem17  34379  poimirlem19  34381  poimirlem20  34382  poimirlem24  34386  poimirlem28  34390  mblfinlem2  34400  mblfinlem4  34402  ismblfin  34403  el3v2  34966  atlatle  35930  pmaple  36371  dihglblem2N  37904  expgcd  38644  elnnrabdioph  38829  rabren3dioph  38837  zindbi  38968  expgrowth  40112  binomcxplemnotnn0  40133  trelpss  40235  etransc  42024  mogoldbb  43343  pgrple2abl  43804  aacllem  44294