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  3545  tz7.7  6353  ordin  6357  onfr  6366  fprresex  8264  tfrlem11  8331  phplem2  9143  epfrs  9654  zorng  10428  tsk2  10690  tskcard  10706  gruina  10743  muladd11  11317  00id  11322  ltaddneg  11363  negsub  11443  subneg  11444  muleqadd  11795  diveq0  11820  diveq1  11840  conjmul  11872  recp1lt1  12054  nnsub  12203  addltmul  12391  nnunb  12411  zltp1le  12555  gtndiv  12583  eluzp1m1  12791  zbtwnre  12873  rebtwnz  12874  xnn0le2is012  13175  supxrbnd  13257  divelunit  13424  fznatpl1  13508  flbi2  13751  fldiv  13794  modid  13830  modm1p1mod0  13859  fzen2  13906  nn0ennn  13916  seqshft2  13965  seqf1olem1  13978  ser1const  13995  sq01  14162  expnbnd  14169  faclbnd3  14229  faclbnd5  14235  hashunsng  14329  hashunsngx  14330  hashxplem  14370  ccatrid  14525  ccats1val1  14564  ccat2s1fst  14577  sgnn  15031  01sqrexlem2  15180  01sqrexlem7  15185  leabs  15236  abs2dif  15270  cvgrat  15820  cos2t  16117  sin01gt0  16129  cos01gt0  16130  demoivre  16139  demoivreALT  16140  rpnnen2lem5  16157  rpnnen2lem12  16164  omeo  16307  gcd0id  16460  sqgcd  16503  expgcd  16504  isprm3  16624  eulerthlem2  16723  pczpre  16789  pcrec  16800  ressress  17188  mulgm1  19041  unitgrpid  20338  mdet0pr  22553  m2detleib  22592  cmpcov2  23351  ufileu  23880  tgpconncompeqg  24073  itg2ge0  25709  mdegldg  26044  abssinper  26503  ppiub  27188  chtub  27196  bposlem2  27269  lgs1  27325  cofcutr  27937  addbday  28031  negbdaylem  28069  precsexlem10  28229  oncutlt  28277  n0bday  28365  bdayn0p1  28382  eucliddivs  28389  nnzs  28399  bdaypw2n0bndlem  28476  zz12s  28488  remulscllem1  28513  colinearalglem4  29000  axsegconlem1  29008  axpaschlem  29031  axcontlem2  29056  axcontlem4  29058  axcontlem7  29061  axcontlem8  29062  funvtxval  29109  funiedgval  29110  vc0  30668  vcm  30670  nvmval2  30737  nvmf  30739  nvmdi  30742  nvnegneg  30743  nvpncan2  30747  nvaddsub4  30751  nvm1  30759  nvdif  30760  nvpi  30761  nvz0  30762  nvmtri  30765  nvabs  30766  nvge0  30767  imsmetlem  30784  4ipval2  30802  ipval3  30803  ipidsq  30804  dipcj  30808  sspmval  30827  ipasslem1  30925  ipasslem2  30926  dipsubdir  30942  hvsubdistr1  31143  shsubcl  31314  shsel3  31409  shunssi  31462  hosubdi  31902  lnopmi  32094  nmophmi  32125  nmopcoi  32189  opsqrlem6  32239  hstle  32324  hst0  32327  mdsl2i  32416  superpos  32448  dmdbr5ati  32516  f1rnen  32724  resvsca  33431  noinfepfnregs  35316  pthhashvtx  35350  cvmliftphtlem  35539  topdifinffinlem  37629  finixpnum  37885  tan2h  37892  poimirlem3  37903  poimirlem4  37904  poimirlem7  37907  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem20  37920  poimirlem24  37924  poimirlem28  37928  mblfinlem2  37938  mblfinlem4  37940  ismblfin  37941  el3v2  38511  atlatle  39725  pmaple  40166  dihglblem2N  41699  sn-ltaddneg  42853  elnnrabdioph  43193  rabren3dioph  43201  zindbi  43332  expgrowth  44720  binomcxplemnotnn0  44741  trelpss  44839  etransc  46670  mogoldbb  48174  pgrple2abl  48754  aacllem  50189