Theorem mp3an2 1452

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 385  df-3an 1056

This theorem is referenced by:  mp3anl2  1459  tz7.7  5787  ordin  5791  onfr  5801  wfrlem14  7473  wfrlem17  7476  tfrlem11  7529  epfrs  8645  zorng  9364  tsk2  9625  tskcard  9641  gruina  9678  muladd11  10244  00id  10249  ltaddneg  10289  negsub  10367  subneg  10368  muleqadd  10709  diveq1  10756  conjmul  10780  recp1lt1  10959  nnsub  11097  addltmul  11306  nnunb  11326  zltp1le  11465  gtndiv  11492  eluzp1m1  11749  zbtwnre  11824  rebtwnz  11825  xnn0le2is012  12114  supxrbnd  12196  divelunit  12352  fznatpl1  12433  flbi2  12658  fldiv  12699  modid  12735  modm1p1mod0  12761  fzen2  12808  nn0ennn  12818  seqshft2  12867  seqf1olem1  12880  ser1const  12897  sq01  13026  expnbnd  13033  faclbnd3  13119  faclbnd5  13125  hashunsng  13219  hashxplem  13258  ccatrid  13405  sgnn  13878  sqrlem2  14028  sqrlem7  14033  leabs  14083  abs2dif  14116  cvgrat  14659  cos2t  14952  sin01gt0  14964  cos01gt0  14965  demoivre  14974  demoivreALT  14975  znnenlem  14984  rpnnen2lem5  14991  rpnnen2lem12  14998  omeo  15137  gcd0id  15287  sqgcd  15325  isprm3  15443  eulerthlem2  15534  pczpre  15599  pcrec  15610  ressress  15985  mulgm1  17609  unitgrpid  18715  mdet0pr  20446  m2detleib  20485  cmpcov2  21241  ufileu  21770  tgpconncompeqg  21962  itg2ge0  23547  mdegldg  23871  abssinper  24315  ppiub  24974  chtub  24982  bposlem2  25055  lgs1  25111  colinearalglem4  25834  axsegconlem1  25842  axpaschlem  25865  axcontlem2  25890  axcontlem4  25892  axcontlem7  25895  axcontlem8  25896  funvtxval  25950  funiedgval  25951  vc0  27557  vcm  27559  nvmval2  27626  nvmf  27628  nvmdi  27631  nvnegneg  27632  nvpncan2  27636  nvaddsub4  27640  nvm1  27648  nvdif  27649  nvpi  27650  nvz0  27651  nvmtri  27654  nvabs  27655  nvge0  27656  imsmetlem  27673  4ipval2  27691  ipval3  27692  ipidsq  27693  dipcj  27697  sspmval  27716  ipasslem1  27814  ipasslem2  27815  dipsubdir  27831  hvsubdistr1  28034  shsubcl  28205  shsel3  28302  shunssi  28355  hosubdi  28795  lnopmi  28987  nmophmi  29018  nmopcoi  29082  opsqrlem6  29132  hstle  29217  hst0  29220  mdsl2i  29309  superpos  29341  dmdbr5ati  29409  resvsca  29958  cvmliftphtlem  31425  topdifinffinlem  33325  finixpnum  33524  tan2h  33531  poimirlem3  33542  poimirlem4  33543  poimirlem7  33546  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem24  33563  poimirlem28  33567  mblfinlem2  33577  mblfinlem4  33579  ismblfin  33580  el3v2  34132  atlatle  34925  pmaple  35365  dihglblem2N  36900  elnnrabdioph  37688  rabren3dioph  37696  zindbi  37828  expgrowth  38851  binomcxplemnotnn0  38872  trelpss  38976  etransc  40818  mogoldbb  41998  pgrple2abl  42471  aacllem  42875