Theorem mp3an2 1446

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 700	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  1453  vtoclegft  3571  tz7.7  6395  ordin  6399  onfr  6408  fprresex  8316  wfrlem14OLD  8343  wfrlem17OLD  8346  tfrlem11  8409  phplem2  9233  epfrs  9755  zorng  10528  tsk2  10789  tskcard  10805  gruina  10842  muladd11  11415  00id  11420  ltaddneg  11460  negsub  11539  subneg  11540  muleqadd  11889  diveq1  11936  conjmul  11962  recp1lt1  12143  nnsub  12287  addltmul  12479  nnunb  12499  zltp1le  12643  gtndiv  12670  eluzp1m1  12879  zbtwnre  12961  rebtwnz  12962  xnn0le2is012  13258  supxrbnd  13340  divelunit  13504  fznatpl1  13588  flbi2  13815  fldiv  13858  modid  13894  modm1p1mod0  13920  fzen2  13967  nn0ennn  13977  seqshft2  14026  seqf1olem1  14039  ser1const  14056  sq01  14220  expnbnd  14227  faclbnd3  14284  faclbnd5  14290  hashunsng  14384  hashunsngx  14385  hashxplem  14425  ccatrid  14570  ccats1val1  14609  ccat2s1fst  14622  sgnn  15074  01sqrexlem2  15223  01sqrexlem7  15228  leabs  15279  abs2dif  15312  cvgrat  15862  cos2t  16155  sin01gt0  16167  cos01gt0  16168  demoivre  16177  demoivreALT  16178  rpnnen2lem5  16195  rpnnen2lem12  16202  omeo  16343  gcd0id  16494  sqgcd  16536  isprm3  16654  eulerthlem2  16751  pczpre  16816  pcrec  16827  ressress  17229  mulgm1  19049  unitgrpid  20324  mdet0pr  22507  m2detleib  22546  cmpcov2  23307  ufileu  23836  tgpconncompeqg  24029  itg2ge0  25678  mdegldg  26015  abssinper  26468  ppiub  27150  chtub  27158  bposlem2  27231  lgs1  27287  cofcutr  27857  negsbdaylem  27981  precsexlem10  28127  n0sbday  28230  remulscllem1  28241  colinearalglem4  28733  axsegconlem1  28741  axpaschlem  28764  axcontlem2  28789  axcontlem4  28791  axcontlem7  28794  axcontlem8  28795  funvtxval  28844  funiedgval  28845  vc0  30397  vcm  30399  nvmval2  30466  nvmf  30468  nvmdi  30471  nvnegneg  30472  nvpncan2  30476  nvaddsub4  30480  nvm1  30488  nvdif  30489  nvpi  30490  nvz0  30491  nvmtri  30494  nvabs  30495  nvge0  30496  imsmetlem  30513  4ipval2  30531  ipval3  30532  ipidsq  30533  dipcj  30537  sspmval  30556  ipasslem1  30654  ipasslem2  30655  dipsubdir  30671  hvsubdistr1  30872  shsubcl  31043  shsel3  31138  shunssi  31191  hosubdi  31631  lnopmi  31823  nmophmi  31854  nmopcoi  31918  opsqrlem6  31968  hstle  32053  hst0  32056  mdsl2i  32145  superpos  32177  dmdbr5ati  32245  f1rnen  32427  resvsca  33054  pthhashvtx  34737  cvmliftphtlem  34927  topdifinffinlem  36826  finixpnum  37078  tan2h  37085  poimirlem3  37096  poimirlem4  37097  poimirlem7  37100  poimirlem16  37109  poimirlem17  37110  poimirlem19  37112  poimirlem20  37113  poimirlem24  37117  poimirlem28  37121  mblfinlem2  37131  mblfinlem4  37133  ismblfin  37134  el3v2  37693  atlatle  38792  pmaple  39234  dihglblem2N  40767  expgcd  41894  sn-ltaddneg  41997  elnnrabdioph  42227  rabren3dioph  42235  zindbi  42367  expgrowth  43772  binomcxplemnotnn0  43793  trelpss  43892  etransc  45671  mogoldbb  47125  pgrple2abl  47429  aacllem  48234