Theorem mp3an2 1451

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

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

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 1088

This theorem is referenced by:  mp3anl2  1458  vtoclegft  3543  tz7.7  6333  ordin  6337  onfr  6346  fprresex  8243  tfrlem11  8310  phplem2  9119  epfrs  9627  zorng  10398  tsk2  10659  tskcard  10675  gruina  10712  muladd11  11286  00id  11291  ltaddneg  11332  negsub  11412  subneg  11413  muleqadd  11764  diveq0  11789  diveq1  11809  conjmul  11841  recp1lt1  12023  nnsub  12172  addltmul  12360  nnunb  12380  zltp1le  12525  gtndiv  12553  eluzp1m1  12761  zbtwnre  12847  rebtwnz  12848  xnn0le2is012  13148  supxrbnd  13230  divelunit  13397  fznatpl1  13481  flbi2  13721  fldiv  13764  modid  13800  modm1p1mod0  13829  fzen2  13876  nn0ennn  13886  seqshft2  13935  seqf1olem1  13948  ser1const  13965  sq01  14132  expnbnd  14139  faclbnd3  14199  faclbnd5  14205  hashunsng  14299  hashunsngx  14300  hashxplem  14340  ccatrid  14494  ccats1val1  14533  ccat2s1fst  14546  sgnn  15001  01sqrexlem2  15150  01sqrexlem7  15155  leabs  15206  abs2dif  15240  cvgrat  15790  cos2t  16087  sin01gt0  16099  cos01gt0  16100  demoivre  16109  demoivreALT  16110  rpnnen2lem5  16127  rpnnen2lem12  16134  omeo  16277  gcd0id  16430  sqgcd  16473  expgcd  16474  isprm3  16594  eulerthlem2  16693  pczpre  16759  pcrec  16770  ressress  17158  mulgm1  18973  unitgrpid  20270  mdet0pr  22477  m2detleib  22516  cmpcov2  23275  ufileu  23804  tgpconncompeqg  23997  itg2ge0  25634  mdegldg  25969  abssinper  26428  ppiub  27113  chtub  27121  bposlem2  27194  lgs1  27250  cofcutr  27839  addsbday  27931  negsbdaylem  27969  precsexlem10  28125  onscutlt  28172  n0sbday  28251  bdayn0p1  28265  eucliddivs  28272  nnzs  28281  zzs12  28356  remulscllem1  28373  colinearalglem4  28858  axsegconlem1  28866  axpaschlem  28889  axcontlem2  28914  axcontlem4  28916  axcontlem7  28919  axcontlem8  28920  funvtxval  28967  funiedgval  28968  vc0  30522  vcm  30524  nvmval2  30591  nvmf  30593  nvmdi  30596  nvnegneg  30597  nvpncan2  30601  nvaddsub4  30605  nvm1  30613  nvdif  30614  nvpi  30615  nvz0  30616  nvmtri  30619  nvabs  30620  nvge0  30621  imsmetlem  30638  4ipval2  30656  ipval3  30657  ipidsq  30658  dipcj  30662  sspmval  30681  ipasslem1  30779  ipasslem2  30780  dipsubdir  30796  hvsubdistr1  30997  shsubcl  31168  shsel3  31263  shunssi  31316  hosubdi  31756  lnopmi  31948  nmophmi  31979  nmopcoi  32043  opsqrlem6  32093  hstle  32178  hst0  32181  mdsl2i  32270  superpos  32302  dmdbr5ati  32370  f1rnen  32579  resvsca  33279  pthhashvtx  35121  cvmliftphtlem  35310  topdifinffinlem  37341  finixpnum  37605  tan2h  37612  poimirlem3  37623  poimirlem4  37624  poimirlem7  37627  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem20  37640  poimirlem24  37644  poimirlem28  37648  mblfinlem2  37658  mblfinlem4  37660  ismblfin  37661  el3v2  38219  atlatle  39319  pmaple  39760  dihglblem2N  41293  sn-ltaddneg  42447  elnnrabdioph  42800  rabren3dioph  42808  zindbi  42939  expgrowth  44328  binomcxplemnotnn0  44349  trelpss  44448  etransc  46284  mogoldbb  47789  pgrple2abl  48369  aacllem  49806