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  3554  tz7.7  6358  ordin  6362  onfr  6371  fprresex  8289  tfrlem11  8356  phplem2  9169  epfrs  9684  zorng  10457  tsk2  10718  tskcard  10734  gruina  10771  muladd11  11344  00id  11349  ltaddneg  11390  negsub  11470  subneg  11471  muleqadd  11822  diveq0  11847  diveq1  11867  conjmul  11899  recp1lt1  12081  nnsub  12230  addltmul  12418  nnunb  12438  zltp1le  12583  gtndiv  12611  eluzp1m1  12819  zbtwnre  12905  rebtwnz  12906  xnn0le2is012  13206  supxrbnd  13288  divelunit  13455  fznatpl1  13539  flbi2  13779  fldiv  13822  modid  13858  modm1p1mod0  13887  fzen2  13934  nn0ennn  13944  seqshft2  13993  seqf1olem1  14006  ser1const  14023  sq01  14190  expnbnd  14197  faclbnd3  14257  faclbnd5  14263  hashunsng  14357  hashunsngx  14358  hashxplem  14398  ccatrid  14552  ccats1val1  14591  ccat2s1fst  14604  sgnn  15060  01sqrexlem2  15209  01sqrexlem7  15214  leabs  15265  abs2dif  15299  cvgrat  15849  cos2t  16146  sin01gt0  16158  cos01gt0  16159  demoivre  16168  demoivreALT  16169  rpnnen2lem5  16186  rpnnen2lem12  16193  omeo  16336  gcd0id  16489  sqgcd  16532  expgcd  16533  isprm3  16653  eulerthlem2  16752  pczpre  16818  pcrec  16829  ressress  17217  mulgm1  19026  unitgrpid  20294  mdet0pr  22479  m2detleib  22518  cmpcov2  23277  ufileu  23806  tgpconncompeqg  23999  itg2ge0  25636  mdegldg  25971  abssinper  26430  ppiub  27115  chtub  27123  bposlem2  27196  lgs1  27252  cofcutr  27832  addsbday  27924  negsbdaylem  27962  precsexlem10  28118  onscutlt  28165  n0sbday  28244  bdayn0p1  28258  eucliddivs  28265  nnzs  28274  zzs12  28339  remulscllem1  28351  colinearalglem4  28836  axsegconlem1  28844  axpaschlem  28867  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  funvtxval  28945  funiedgval  28946  vc0  30503  vcm  30505  nvmval2  30572  nvmf  30574  nvmdi  30577  nvnegneg  30578  nvpncan2  30582  nvaddsub4  30586  nvm1  30594  nvdif  30595  nvpi  30596  nvz0  30597  nvmtri  30600  nvabs  30601  nvge0  30602  imsmetlem  30619  4ipval2  30637  ipval3  30638  ipidsq  30639  dipcj  30643  sspmval  30662  ipasslem1  30760  ipasslem2  30761  dipsubdir  30777  hvsubdistr1  30978  shsubcl  31149  shsel3  31244  shunssi  31297  hosubdi  31737  lnopmi  31929  nmophmi  31960  nmopcoi  32024  opsqrlem6  32074  hstle  32159  hst0  32162  mdsl2i  32251  superpos  32283  dmdbr5ati  32351  f1rnen  32553  resvsca  33304  pthhashvtx  35115  cvmliftphtlem  35304  topdifinffinlem  37335  finixpnum  37599  tan2h  37606  poimirlem3  37617  poimirlem4  37618  poimirlem7  37621  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem24  37638  poimirlem28  37642  mblfinlem2  37652  mblfinlem4  37654  ismblfin  37655  el3v2  38213  atlatle  39313  pmaple  39755  dihglblem2N  41288  sn-ltaddneg  42442  elnnrabdioph  42795  rabren3dioph  42803  zindbi  42935  expgrowth  44324  binomcxplemnotnn0  44345  trelpss  44444  etransc  46281  mogoldbb  47786  pgrple2abl  48353  aacllem  49790