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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  mp3anl2  1459  vtoclegft  3544  tz7.7  6344  ordin  6348  onfr  6357  fprresex  8254  tfrlem11  8321  phplem2  9133  epfrs  9644  zorng  10418  tsk2  10680  tskcard  10696  gruina  10733  muladd11  11307  00id  11312  ltaddneg  11353  negsub  11433  subneg  11434  muleqadd  11785  diveq0  11810  diveq1  11830  conjmul  11862  recp1lt1  12044  nnsub  12193  addltmul  12381  nnunb  12401  zltp1le  12545  gtndiv  12573  eluzp1m1  12781  zbtwnre  12863  rebtwnz  12864  xnn0le2is012  13165  supxrbnd  13247  divelunit  13414  fznatpl1  13498  flbi2  13741  fldiv  13784  modid  13820  modm1p1mod0  13849  fzen2  13896  nn0ennn  13906  seqshft2  13955  seqf1olem1  13968  ser1const  13985  sq01  14152  expnbnd  14159  faclbnd3  14219  faclbnd5  14225  hashunsng  14319  hashunsngx  14320  hashxplem  14360  ccatrid  14515  ccats1val1  14554  ccat2s1fst  14567  sgnn  15021  01sqrexlem2  15170  01sqrexlem7  15175  leabs  15226  abs2dif  15260  cvgrat  15810  cos2t  16107  sin01gt0  16119  cos01gt0  16120  demoivre  16129  demoivreALT  16130  rpnnen2lem5  16147  rpnnen2lem12  16154  omeo  16297  gcd0id  16450  sqgcd  16493  expgcd  16494  isprm3  16614  eulerthlem2  16713  pczpre  16779  pcrec  16790  ressress  17178  mulgm1  19028  unitgrpid  20325  mdet0pr  22540  m2detleib  22579  cmpcov2  23338  ufileu  23867  tgpconncompeqg  24060  itg2ge0  25696  mdegldg  26031  abssinper  26490  ppiub  27175  chtub  27183  bposlem2  27256  lgs1  27312  cofcutr  27924  addbday  28018  negbdaylem  28056  precsexlem10  28216  oncutlt  28264  n0bday  28352  bdayn0p1  28369  eucliddivs  28376  nnzs  28386  bdaypw2n0bndlem  28463  zz12s  28475  remulscllem1  28500  colinearalglem4  28986  axsegconlem1  28994  axpaschlem  29017  axcontlem2  29042  axcontlem4  29044  axcontlem7  29047  axcontlem8  29048  funvtxval  29095  funiedgval  29096  vc0  30653  vcm  30655  nvmval2  30722  nvmf  30724  nvmdi  30727  nvnegneg  30728  nvpncan2  30732  nvaddsub4  30736  nvm1  30744  nvdif  30745  nvpi  30746  nvz0  30747  nvmtri  30750  nvabs  30751  nvge0  30752  imsmetlem  30769  4ipval2  30787  ipval3  30788  ipidsq  30789  dipcj  30793  sspmval  30812  ipasslem1  30910  ipasslem2  30911  dipsubdir  30927  hvsubdistr1  31128  shsubcl  31299  shsel3  31394  shunssi  31447  hosubdi  31887  lnopmi  32079  nmophmi  32110  nmopcoi  32174  opsqrlem6  32224  hstle  32309  hst0  32312  mdsl2i  32401  superpos  32433  dmdbr5ati  32501  f1rnen  32709  resvsca  33415  noinfepfnregs  35290  pthhashvtx  35324  cvmliftphtlem  35513  topdifinffinlem  37554  finixpnum  37808  tan2h  37815  poimirlem3  37826  poimirlem4  37827  poimirlem7  37830  poimirlem16  37839  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem24  37847  poimirlem28  37851  mblfinlem2  37861  mblfinlem4  37863  ismblfin  37864  el3v2  38434  atlatle  39648  pmaple  40089  dihglblem2N  41622  sn-ltaddneg  42776  elnnrabdioph  43116  rabren3dioph  43124  zindbi  43255  expgrowth  44643  binomcxplemnotnn0  44664  trelpss  44762  etransc  46594  mogoldbb  48098  pgrple2abl  48678  aacllem  50113