Theorem mp3an2 1449

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 699	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087

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 398  df-3an 1089

This theorem is referenced by:  mp3anl2  1456  tz7.7  6307  ordin  6311  onfr  6320  fprresex  8157  wfrlem14OLD  8184  wfrlem17OLD  8187  tfrlem11  8250  phplem2  9029  epfrs  9533  zorng  10306  tsk2  10567  tskcard  10583  gruina  10620  muladd11  11191  00id  11196  ltaddneg  11236  negsub  11315  subneg  11316  muleqadd  11665  diveq1  11712  conjmul  11738  recp1lt1  11919  nnsub  12063  addltmul  12255  nnunb  12275  zltp1le  12416  gtndiv  12443  eluzp1m1  12654  zbtwnre  12732  rebtwnz  12733  xnn0le2is012  13026  supxrbnd  13108  divelunit  13272  fznatpl1  13356  flbi2  13583  fldiv  13626  modid  13662  modm1p1mod0  13688  fzen2  13735  nn0ennn  13745  seqshft2  13795  seqf1olem1  13808  ser1const  13825  sq01  13986  expnbnd  13993  faclbnd3  14052  faclbnd5  14058  hashunsng  14152  hashunsngx  14153  hashxplem  14193  ccatrid  14337  ccats1val1  14377  ccat2s1fst  14396  sgnn  14850  sqrlem2  15000  sqrlem7  15005  leabs  15056  abs2dif  15089  cvgrat  15640  cos2t  15932  sin01gt0  15944  cos01gt0  15945  demoivre  15954  demoivreALT  15955  rpnnen2lem5  15972  rpnnen2lem12  15979  omeo  16120  gcd0id  16271  sqgcd  16315  isprm3  16433  eulerthlem2  16528  pczpre  16593  pcrec  16604  ressress  17003  mulgm1  18769  unitgrpid  19956  mdet0pr  21786  m2detleib  21825  cmpcov2  22586  ufileu  23115  tgpconncompeqg  23308  itg2ge0  24945  mdegldg  25276  abssinper  25722  ppiub  26397  chtub  26405  bposlem2  26478  lgs1  26534  colinearalglem4  27322  axsegconlem1  27330  axpaschlem  27353  axcontlem2  27378  axcontlem4  27380  axcontlem7  27383  axcontlem8  27384  funvtxval  27433  funiedgval  27434  vc0  28981  vcm  28983  nvmval2  29050  nvmf  29052  nvmdi  29055  nvnegneg  29056  nvpncan2  29060  nvaddsub4  29064  nvm1  29072  nvdif  29073  nvpi  29074  nvz0  29075  nvmtri  29078  nvabs  29079  nvge0  29080  imsmetlem  29097  4ipval2  29115  ipval3  29116  ipidsq  29117  dipcj  29121  sspmval  29140  ipasslem1  29238  ipasslem2  29239  dipsubdir  29255  hvsubdistr1  29456  shsubcl  29627  shsel3  29722  shunssi  29775  hosubdi  30215  lnopmi  30407  nmophmi  30438  nmopcoi  30502  opsqrlem6  30552  hstle  30637  hst0  30640  mdsl2i  30729  superpos  30761  dmdbr5ati  30829  f1rnen  31009  resvsca  31574  pthhashvtx  33134  cvmliftphtlem  33324  cofcutr  34137  topdifinffinlem  35562  finixpnum  35806  tan2h  35813  poimirlem3  35824  poimirlem4  35825  poimirlem7  35828  poimirlem16  35837  poimirlem17  35838  poimirlem19  35840  poimirlem20  35841  poimirlem24  35845  poimirlem28  35849  mblfinlem2  35859  mblfinlem4  35861  ismblfin  35862  el3v2  36417  atlatle  37376  pmaple  37817  dihglblem2N  39350  expgcd  40371  elnnrabdioph  40666  rabren3dioph  40674  zindbi  40806  expgrowth  41991  binomcxplemnotnn0  42012  trelpss  42111  etransc  43873  mogoldbb  45295  pgrple2abl  45759  aacllem  46563