Theorem mp3an2 1478

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3anl2  1485  vtoclegft  3543  tz7.7  6388  ordin  6393  onfr  6402  fprresex  8328  tfrlem11  8396  phplem2  9220  epfrs  9732  zorng  10582  tsk2  10850  tskcard  10866  gruina  10903  muladd11  11480  00id  11485  ltaddneg  11526  negsub  11606  subneg  11607  muleqadd  11960  diveq0  11984  diveq1  12003  conjmul  12034  recp1lt1  12215  nnsub  12382  addltmul  12582  nnunb  12602  zltp1le  12746  gtndiv  12776  eluzp1m1  12991  zbtwnre  13073  rebtwnz  13074  xnn0le2is012  13376  supxrbnd  13458  divelunit  13625  fznatpl1  13712  flbi2  13957  fldiv  14000  modid  14036  modm1p1mod0  14065  fzen2  14112  nn0ennn  14122  seqshft2  14171  seqf1olem1  14184  ser1const  14201  sq01  14369  expnbnd  14376  faclbnd3  14436  faclbnd5  14442  hashunsng  14536  hashunsngx  14537  hashxplem  14578  ccatrid  14733  ccats1val1  14774  ccat2s1fst  14787  sgnn  15247  01sqrexlem2  15410  01sqrexlem7  15415  leabs  15466  abs2dif  15500  cvgrat  16052  cos2t  16346  sin01gt0  16358  cos01gt0  16359  demoivre  16368  demoivreALT  16369  rpnnen2lem5  16386  rpnnen2lem12  16393  omeo  16536  gcd0id  16691  sqgcd  16736  expgcd  16737  isprm3  16858  eulerthlem2  16959  pczpre  17025  pcrec  17036  ressress  17425  mulgm1  19304  unitgrpid  20615  mdet0pr  22907  m2detleib  22946  cmpcov2  23708  ufileu  24238  tgpconncompeqg  24431  itg2ge0  26056  mdegldg  26384  abssinper  26849  ppiub  27531  chtub  27539  bposlem2  27612  lgs1  27668  cofcutr  28310  addbday  28404  negbdaylem  28442  precsexlem10  28602  oncutlt  28650  n0bday  28738  bdayn0p1  28755  eucliddivs  28762  nnzs  28772  bdaypw2n0bndlem  28849  zz12s  28861  remulscllem1  28886  colinearalglem4  29487  axsegconlem1  29495  axpaschlem  29518  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem8  29549  funvtxval  29596  funiedgval  29597  pthhashvtx  30315  vc0  31176  vcm  31178  nvmval2  31245  nvmf  31247  nvmdi  31250  nvnegneg  31251  nvpncan2  31255  nvaddsub4  31259  nvm1  31267  nvdif  31268  nvpi  31269  nvz0  31270  nvmtri  31273  nvabs  31274  nvge0  31275  imsmetlem  31292  4ipval2  31310  ipval3  31311  ipidsq  31312  dipcj  31316  sspmval  31335  ipasslem1  31433  ipasslem2  31434  dipsubdir  31450  hvsubdistr1  31651  shsubcl  31822  shsel3  31917  shunssi  31970  hosubdi  32410  lnopmi  32602  nmophmi  32633  nmopcoi  32697  opsqrlem6  32747  hstle  32832  hst0  32835  mdsl2i  32924  superpos  32956  dmdbr5ati  33024  f1rnen  33222  resvsca  33893  weexenwe  35756  noinfepfnregs  35800  vonf1onprcf1ac  35894  cvmliftphtlem  36082  mh-inf3f1  37329  topdifinffinlem  38271  finixpnum  38529  tan2h  38536  poimirlem3  38542  poimirlem4  38543  poimirlem7  38546  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  poimirlem24  38563  poimirlem28  38567  mblfinlem2  38577  mblfinlem4  38579  ismblfin  38580  el3v2  39164  atlatle  40378  pmaple  40819  dihglblem2N  42352  sn-ltaddneg  43519  elnnrabdioph  43814  rabren3dioph  43822  zindbi  43953  expgrowth  45319  binomcxplemnotnn0  45340  trelpss  45437  etransc  47293  mogoldbb  48883  pgrple2abl  49477  aacllem  50939