Theorem mp3an2 1472

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  mp3anl2  1479  vtoclegft  3550  tz7.7  6374  ordin  6378  onfr  6387  fprresex  8293  tfrlem11  8361  phplem2  9175  epfrs  9688  zorng  10463  tsk2  10725  tskcard  10741  gruina  10778  muladd11  11355  00id  11360  ltaddneg  11401  negsub  11481  subneg  11482  muleqadd  11833  diveq0  11857  diveq1  11877  conjmul  11910  recp1lt1  12092  nnsub  12259  addltmul  12459  nnunb  12479  zltp1le  12623  gtndiv  12652  eluzp1m1  12867  zbtwnre  12949  rebtwnz  12950  xnn0le2is012  13251  supxrbnd  13333  divelunit  13500  fznatpl1  13585  flbi2  13829  fldiv  13872  modid  13908  modm1p1mod0  13937  fzen2  13984  nn0ennn  13994  seqshft2  14043  seqf1olem1  14056  ser1const  14073  sq01  14240  expnbnd  14247  faclbnd3  14307  faclbnd5  14313  hashunsng  14407  hashunsngx  14408  hashxplem  14448  ccatrid  14603  ccats1val1  14642  ccat2s1fst  14655  sgnn  15109  01sqrexlem2  15272  01sqrexlem7  15277  leabs  15328  abs2dif  15362  cvgrat  15915  cos2t  16212  sin01gt0  16224  cos01gt0  16225  demoivre  16234  demoivreALT  16235  rpnnen2lem5  16252  rpnnen2lem12  16259  omeo  16402  gcd0id  16555  sqgcd  16598  expgcd  16599  isprm3  16719  eulerthlem2  16819  pczpre  16885  pcrec  16896  ressress  17285  mulgm1  19138  unitgrpid  20436  mdet0pr  22654  m2detleib  22693  cmpcov2  23452  ufileu  23981  tgpconncompeqg  24174  itg2ge0  25799  mdegldg  26128  abssinper  26588  ppiub  27270  chtub  27278  bposlem2  27351  lgs1  27407  cofcutr  28019  addbday  28113  negbdaylem  28151  precsexlem10  28311  oncutlt  28359  n0bday  28447  bdayn0p1  28464  eucliddivs  28471  nnzs  28481  bdaypw2n0bndlem  28558  zz12s  28570  remulscllem1  28595  colinearalglem4  29112  axsegconlem1  29120  axpaschlem  29143  axcontlem2  29168  axcontlem4  29170  axcontlem7  29173  axcontlem8  29174  funvtxval  29221  funiedgval  29222  vc0  30779  vcm  30781  nvmval2  30848  nvmf  30850  nvmdi  30853  nvnegneg  30854  nvpncan2  30858  nvaddsub4  30862  nvm1  30870  nvdif  30871  nvpi  30872  nvz0  30873  nvmtri  30876  nvabs  30877  nvge0  30878  imsmetlem  30895  4ipval2  30913  ipval3  30914  ipidsq  30915  dipcj  30919  sspmval  30938  ipasslem1  31036  ipasslem2  31037  dipsubdir  31053  hvsubdistr1  31254  shsubcl  31425  shsel3  31520  shunssi  31573  hosubdi  32013  lnopmi  32205  nmophmi  32236  nmopcoi  32300  opsqrlem6  32350  hstle  32435  hst0  32438  mdsl2i  32527  superpos  32559  dmdbr5ati  32627  f1rnen  32832  resvsca  33520  noinfepfnregs  35432  pthhashvtx  35483  cvmliftphtlem  35672  topdifinffinlem  37846  finixpnum  38109  tan2h  38116  poimirlem3  38127  poimirlem4  38128  poimirlem7  38131  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem24  38148  poimirlem28  38152  mblfinlem2  38162  mblfinlem4  38164  ismblfin  38165  el3v2  38735  atlatle  39949  pmaple  40390  dihglblem2N  41923  sn-ltaddneg  43081  elnnrabdioph  43389  rabren3dioph  43397  zindbi  43528  expgrowth  44916  binomcxplemnotnn0  44937  trelpss  45035  etransc  46862  mogoldbb  48412  pgrple2abl  48992  aacllem  50427