Theorem mp3an2 1448

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 1117	. 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  1455  vtoclegft  3587  tz7.7  6411  ordin  6415  onfr  6424  fprresex  8333  wfrlem14OLD  8360  wfrlem17OLD  8363  tfrlem11  8426  phplem2  9242  epfrs  9768  zorng  10541  tsk2  10802  tskcard  10818  gruina  10855  muladd11  11428  00id  11433  ltaddneg  11474  negsub  11554  subneg  11555  muleqadd  11904  diveq0  11929  diveq1  11949  conjmul  11981  recp1lt1  12163  nnsub  12307  addltmul  12499  nnunb  12519  zltp1le  12664  gtndiv  12692  eluzp1m1  12901  zbtwnre  12985  rebtwnz  12986  xnn0le2is012  13284  supxrbnd  13366  divelunit  13530  fznatpl1  13614  flbi2  13853  fldiv  13896  modid  13932  modm1p1mod0  13959  fzen2  14006  nn0ennn  14016  seqshft2  14065  seqf1olem1  14078  ser1const  14095  sq01  14260  expnbnd  14267  faclbnd3  14327  faclbnd5  14333  hashunsng  14427  hashunsngx  14428  hashxplem  14468  ccatrid  14621  ccats1val1  14660  ccat2s1fst  14673  sgnn  15129  01sqrexlem2  15278  01sqrexlem7  15283  leabs  15334  abs2dif  15367  cvgrat  15915  cos2t  16210  sin01gt0  16222  cos01gt0  16223  demoivre  16232  demoivreALT  16233  rpnnen2lem5  16250  rpnnen2lem12  16257  omeo  16399  gcd0id  16552  sqgcd  16595  expgcd  16596  isprm3  16716  eulerthlem2  16815  pczpre  16880  pcrec  16891  ressress  17293  mulgm1  19124  unitgrpid  20401  mdet0pr  22613  m2detleib  22652  cmpcov2  23413  ufileu  23942  tgpconncompeqg  24135  itg2ge0  25784  mdegldg  26119  abssinper  26577  ppiub  27262  chtub  27270  bposlem2  27343  lgs1  27399  cofcutr  27972  addsbday  28064  negsbdaylem  28102  precsexlem10  28254  n0sbday  28368  nnzs  28386  pw2bday  28432  zzs12  28437  remulscllem1  28446  colinearalglem4  28938  axsegconlem1  28946  axpaschlem  28969  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem8  29000  funvtxval  29049  funiedgval  29050  vc0  30602  vcm  30604  nvmval2  30671  nvmf  30673  nvmdi  30676  nvnegneg  30677  nvpncan2  30681  nvaddsub4  30685  nvm1  30693  nvdif  30694  nvpi  30695  nvz0  30696  nvmtri  30699  nvabs  30700  nvge0  30701  imsmetlem  30718  4ipval2  30736  ipval3  30737  ipidsq  30738  dipcj  30742  sspmval  30761  ipasslem1  30859  ipasslem2  30860  dipsubdir  30876  hvsubdistr1  31077  shsubcl  31248  shsel3  31343  shunssi  31396  hosubdi  31836  lnopmi  32028  nmophmi  32059  nmopcoi  32123  opsqrlem6  32173  hstle  32258  hst0  32261  mdsl2i  32350  superpos  32382  dmdbr5ati  32450  f1rnen  32645  resvsca  33335  pthhashvtx  35111  cvmliftphtlem  35301  topdifinffinlem  37329  finixpnum  37591  tan2h  37598  poimirlem3  37609  poimirlem4  37610  poimirlem7  37613  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem24  37630  poimirlem28  37634  mblfinlem2  37644  mblfinlem4  37646  ismblfin  37647  el3v2  38205  atlatle  39301  pmaple  39743  dihglblem2N  41276  sn-ltaddneg  42448  elnnrabdioph  42794  rabren3dioph  42802  zindbi  42934  expgrowth  44330  binomcxplemnotnn0  44351  trelpss  44450  etransc  46238  mogoldbb  47709  pgrple2abl  48209  aacllem  49031