Theorem mp3an2 1477

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  mp3anl2  1484  vtoclegft  3547  tz7.7  6386  ordin  6391  onfr  6400  fprresex  8305  tfrlem11  8373  phplem2  9187  epfrs  9698  zorng  10494  tsk2  10756  tskcard  10772  gruina  10809  muladd11  11386  00id  11391  ltaddneg  11432  negsub  11512  subneg  11513  muleqadd  11864  diveq0  11888  diveq1  11907  conjmul  11938  recp1lt1  12119  nnsub  12286  addltmul  12486  nnunb  12506  zltp1le  12650  gtndiv  12679  eluzp1m1  12894  zbtwnre  12976  rebtwnz  12977  xnn0le2is012  13278  supxrbnd  13360  divelunit  13527  fznatpl1  13613  flbi2  13857  fldiv  13900  modid  13936  modm1p1mod0  13965  fzen2  14012  nn0ennn  14022  seqshft2  14071  seqf1olem1  14084  ser1const  14101  sq01  14268  expnbnd  14275  faclbnd3  14335  faclbnd5  14341  hashunsng  14435  hashunsngx  14436  hashxplem  14477  ccatrid  14632  ccats1val1  14671  ccat2s1fst  14684  sgnn  15138  01sqrexlem2  15301  01sqrexlem7  15306  leabs  15357  abs2dif  15391  cvgrat  15944  cos2t  16240  sin01gt0  16252  cos01gt0  16253  demoivre  16262  demoivreALT  16263  rpnnen2lem5  16280  rpnnen2lem12  16287  omeo  16430  gcd0id  16583  sqgcd  16626  expgcd  16627  isprm3  16747  eulerthlem2  16847  pczpre  16913  pcrec  16924  ressress  17313  mulgm1  19166  unitgrpid  20474  mdet0pr  22760  m2detleib  22799  cmpcov2  23558  ufileu  24087  tgpconncompeqg  24280  itg2ge0  25905  mdegldg  26234  abssinper  26697  ppiub  27379  chtub  27387  bposlem2  27460  lgs1  27516  cofcutr  28128  addbday  28222  negbdaylem  28260  precsexlem10  28420  oncutlt  28468  n0bday  28556  bdayn0p1  28573  eucliddivs  28580  nnzs  28590  bdaypw2n0bndlem  28667  zz12s  28679  remulscllem1  28704  colinearalglem4  29270  axsegconlem1  29278  axpaschlem  29301  axcontlem2  29326  axcontlem4  29328  axcontlem7  29331  axcontlem8  29332  funvtxval  29379  funiedgval  29380  vc0  30937  vcm  30939  nvmval2  31006  nvmf  31008  nvmdi  31011  nvnegneg  31012  nvpncan2  31016  nvaddsub4  31020  nvm1  31028  nvdif  31029  nvpi  31030  nvz0  31031  nvmtri  31034  nvabs  31035  nvge0  31036  imsmetlem  31053  4ipval2  31071  ipval3  31072  ipidsq  31073  dipcj  31077  sspmval  31096  ipasslem1  31194  ipasslem2  31195  dipsubdir  31211  hvsubdistr1  31412  shsubcl  31583  shsel3  31678  shunssi  31731  hosubdi  32171  lnopmi  32363  nmophmi  32394  nmopcoi  32458  opsqrlem6  32508  hstle  32593  hst0  32596  mdsl2i  32685  superpos  32717  dmdbr5ati  32785  f1rnen  32984  resvsca  33661  noinfepfnregs  35553  pthhashvtx  35628  cvmliftphtlem  35817  topdifinffinlem  38021  finixpnum  38284  tan2h  38291  poimirlem3  38302  poimirlem4  38303  poimirlem7  38306  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem24  38323  poimirlem28  38327  mblfinlem2  38337  mblfinlem4  38339  ismblfin  38340  el3v2  38908  atlatle  40122  pmaple  40563  dihglblem2N  42096  sn-ltaddneg  43256  elnnrabdioph  43562  rabren3dioph  43570  zindbi  43701  expgrowth  45073  binomcxplemnotnn0  45094  trelpss  45191  etransc  47025  mogoldbb  48578  pgrple2abl  49173  aacllem  50649