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  3542  tz7.7  6342  ordin  6346  onfr  6355  fprresex  8252  tfrlem11  8319  phplem2  9131  epfrs  9642  zorng  10416  tsk2  10678  tskcard  10694  gruina  10731  muladd11  11305  00id  11310  ltaddneg  11351  negsub  11431  subneg  11432  muleqadd  11783  diveq0  11808  diveq1  11828  conjmul  11860  recp1lt1  12042  nnsub  12191  addltmul  12379  nnunb  12399  zltp1le  12543  gtndiv  12571  eluzp1m1  12779  zbtwnre  12861  rebtwnz  12862  xnn0le2is012  13163  supxrbnd  13245  divelunit  13412  fznatpl1  13496  flbi2  13739  fldiv  13782  modid  13818  modm1p1mod0  13847  fzen2  13894  nn0ennn  13904  seqshft2  13953  seqf1olem1  13966  ser1const  13983  sq01  14150  expnbnd  14157  faclbnd3  14217  faclbnd5  14223  hashunsng  14317  hashunsngx  14318  hashxplem  14358  ccatrid  14513  ccats1val1  14552  ccat2s1fst  14565  sgnn  15019  01sqrexlem2  15168  01sqrexlem7  15173  leabs  15224  abs2dif  15258  cvgrat  15808  cos2t  16105  sin01gt0  16117  cos01gt0  16118  demoivre  16127  demoivreALT  16128  rpnnen2lem5  16145  rpnnen2lem12  16152  omeo  16295  gcd0id  16448  sqgcd  16491  expgcd  16492  isprm3  16612  eulerthlem2  16711  pczpre  16777  pcrec  16788  ressress  17176  mulgm1  19026  unitgrpid  20323  mdet0pr  22538  m2detleib  22577  cmpcov2  23336  ufileu  23865  tgpconncompeqg  24058  itg2ge0  25694  mdegldg  26029  abssinper  26488  ppiub  27173  chtub  27181  bposlem2  27254  lgs1  27310  cofcutr  27904  addsbday  27998  negsbdaylem  28036  precsexlem10  28195  onscutlt  28243  n0sbday  28330  bdayn0p1  28346  eucliddivs  28353  nnzs  28363  bdaypw2n0sbndlem  28440  zzs12  28452  remulscllem1  28477  colinearalglem4  28963  axsegconlem1  28971  axpaschlem  28994  axcontlem2  29019  axcontlem4  29021  axcontlem7  29024  axcontlem8  29025  funvtxval  29072  funiedgval  29073  vc0  30630  vcm  30632  nvmval2  30699  nvmf  30701  nvmdi  30704  nvnegneg  30705  nvpncan2  30709  nvaddsub4  30713  nvm1  30721  nvdif  30722  nvpi  30723  nvz0  30724  nvmtri  30727  nvabs  30728  nvge0  30729  imsmetlem  30746  4ipval2  30764  ipval3  30765  ipidsq  30766  dipcj  30770  sspmval  30789  ipasslem1  30887  ipasslem2  30888  dipsubdir  30904  hvsubdistr1  31105  shsubcl  31276  shsel3  31371  shunssi  31424  hosubdi  31864  lnopmi  32056  nmophmi  32087  nmopcoi  32151  opsqrlem6  32201  hstle  32286  hst0  32289  mdsl2i  32378  superpos  32410  dmdbr5ati  32478  f1rnen  32686  resvsca  33392  noinfepfnregs  35267  pthhashvtx  35301  cvmliftphtlem  35490  topdifinffinlem  37521  finixpnum  37775  tan2h  37782  poimirlem3  37793  poimirlem4  37794  poimirlem7  37797  poimirlem16  37806  poimirlem17  37807  poimirlem19  37809  poimirlem20  37810  poimirlem24  37814  poimirlem28  37818  mblfinlem2  37828  mblfinlem4  37830  ismblfin  37831  el3v2  38401  atlatle  39615  pmaple  40056  dihglblem2N  41589  sn-ltaddneg  42746  elnnrabdioph  43086  rabren3dioph  43094  zindbi  43225  expgrowth  44613  binomcxplemnotnn0  44634  trelpss  44732  etransc  46564  mogoldbb  48068  pgrple2abl  48648  aacllem  50083