Theorem mp3an2 1447

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  mp3anl2  1454  tz7.7  6289  ordin  6293  onfr  6302  fprresex  8110  wfrlem14OLD  8137  wfrlem17OLD  8140  tfrlem11  8203  phplem2  8955  epfrs  9472  zorng  10244  tsk2  10505  tskcard  10521  gruina  10558  muladd11  11128  00id  11133  ltaddneg  11173  negsub  11252  subneg  11253  muleqadd  11602  diveq1  11649  conjmul  11675  recp1lt1  11856  nnsub  12000  addltmul  12192  nnunb  12212  zltp1le  12353  gtndiv  12380  eluzp1m1  12590  zbtwnre  12668  rebtwnz  12669  xnn0le2is012  12962  supxrbnd  13044  divelunit  13208  fznatpl1  13292  flbi2  13518  fldiv  13561  modid  13597  modm1p1mod0  13623  fzen2  13670  nn0ennn  13680  seqshft2  13730  seqf1olem1  13743  ser1const  13760  sq01  13921  expnbnd  13928  faclbnd3  13987  faclbnd5  13993  hashunsng  14088  hashunsngx  14089  hashxplem  14129  ccatrid  14273  ccats1val1  14313  ccat2s1fst  14332  sgnn  14786  sqrlem2  14936  sqrlem7  14941  leabs  14992  abs2dif  15025  cvgrat  15576  cos2t  15868  sin01gt0  15880  cos01gt0  15881  demoivre  15890  demoivreALT  15891  rpnnen2lem5  15908  rpnnen2lem12  15915  omeo  16056  gcd0id  16207  sqgcd  16251  isprm3  16369  eulerthlem2  16464  pczpre  16529  pcrec  16540  ressress  16939  mulgm1  18705  unitgrpid  19892  mdet0pr  21722  m2detleib  21761  cmpcov2  22522  ufileu  23051  tgpconncompeqg  23244  itg2ge0  24881  mdegldg  25212  abssinper  25658  ppiub  26333  chtub  26341  bposlem2  26414  lgs1  26470  colinearalglem4  27258  axsegconlem1  27266  axpaschlem  27289  axcontlem2  27314  axcontlem4  27316  axcontlem7  27319  axcontlem8  27320  funvtxval  27369  funiedgval  27370  vc0  28915  vcm  28917  nvmval2  28984  nvmf  28986  nvmdi  28989  nvnegneg  28990  nvpncan2  28994  nvaddsub4  28998  nvm1  29006  nvdif  29007  nvpi  29008  nvz0  29009  nvmtri  29012  nvabs  29013  nvge0  29014  imsmetlem  29031  4ipval2  29049  ipval3  29050  ipidsq  29051  dipcj  29055  sspmval  29074  ipasslem1  29172  ipasslem2  29173  dipsubdir  29189  hvsubdistr1  29390  shsubcl  29561  shsel3  29656  shunssi  29709  hosubdi  30149  lnopmi  30341  nmophmi  30372  nmopcoi  30436  opsqrlem6  30486  hstle  30571  hst0  30574  mdsl2i  30663  superpos  30695  dmdbr5ati  30763  f1rnen  30943  resvsca  31508  pthhashvtx  33068  cvmliftphtlem  33258  cofcutr  34071  topdifinffinlem  35497  finixpnum  35741  tan2h  35748  poimirlem3  35759  poimirlem4  35760  poimirlem7  35763  poimirlem16  35772  poimirlem17  35773  poimirlem19  35775  poimirlem20  35776  poimirlem24  35780  poimirlem28  35784  mblfinlem2  35794  mblfinlem4  35796  ismblfin  35797  el3v2  36352  atlatle  37313  pmaple  37754  dihglblem2N  39287  expgcd  40314  elnnrabdioph  40609  rabren3dioph  40617  zindbi  40748  expgrowth  41906  binomcxplemnotnn0  41927  trelpss  42026  etransc  43778  mogoldbb  45189  pgrple2abl  45653  aacllem  46457