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  3551  tz7.7  6346  ordin  6350  onfr  6359  fprresex  8266  tfrlem11  8333  phplem2  9146  epfrs  9662  zorng  10435  tsk2  10696  tskcard  10712  gruina  10749  muladd11  11322  00id  11327  ltaddneg  11368  negsub  11448  subneg  11449  muleqadd  11800  diveq0  11825  diveq1  11845  conjmul  11877  recp1lt1  12059  nnsub  12208  addltmul  12396  nnunb  12416  zltp1le  12561  gtndiv  12589  eluzp1m1  12797  zbtwnre  12883  rebtwnz  12884  xnn0le2is012  13184  supxrbnd  13266  divelunit  13433  fznatpl1  13517  flbi2  13757  fldiv  13800  modid  13836  modm1p1mod0  13865  fzen2  13912  nn0ennn  13922  seqshft2  13971  seqf1olem1  13984  ser1const  14001  sq01  14168  expnbnd  14175  faclbnd3  14235  faclbnd5  14241  hashunsng  14335  hashunsngx  14336  hashxplem  14376  ccatrid  14530  ccats1val1  14569  ccat2s1fst  14582  sgnn  15037  01sqrexlem2  15186  01sqrexlem7  15191  leabs  15242  abs2dif  15276  cvgrat  15826  cos2t  16123  sin01gt0  16135  cos01gt0  16136  demoivre  16145  demoivreALT  16146  rpnnen2lem5  16163  rpnnen2lem12  16170  omeo  16313  gcd0id  16466  sqgcd  16509  expgcd  16510  isprm3  16630  eulerthlem2  16729  pczpre  16795  pcrec  16806  ressress  17194  mulgm1  19009  unitgrpid  20306  mdet0pr  22513  m2detleib  22552  cmpcov2  23311  ufileu  23840  tgpconncompeqg  24033  itg2ge0  25670  mdegldg  26005  abssinper  26464  ppiub  27149  chtub  27157  bposlem2  27230  lgs1  27286  cofcutr  27873  addsbday  27965  negsbdaylem  28003  precsexlem10  28159  onscutlt  28206  n0sbday  28285  bdayn0p1  28299  eucliddivs  28306  nnzs  28315  zzs12  28388  remulscllem1  28405  colinearalglem4  28890  axsegconlem1  28898  axpaschlem  28921  axcontlem2  28946  axcontlem4  28948  axcontlem7  28951  axcontlem8  28952  funvtxval  28999  funiedgval  29000  vc0  30554  vcm  30556  nvmval2  30623  nvmf  30625  nvmdi  30628  nvnegneg  30629  nvpncan2  30633  nvaddsub4  30637  nvm1  30645  nvdif  30646  nvpi  30647  nvz0  30648  nvmtri  30651  nvabs  30652  nvge0  30653  imsmetlem  30670  4ipval2  30688  ipval3  30689  ipidsq  30690  dipcj  30694  sspmval  30713  ipasslem1  30811  ipasslem2  30812  dipsubdir  30828  hvsubdistr1  31029  shsubcl  31200  shsel3  31295  shunssi  31348  hosubdi  31788  lnopmi  31980  nmophmi  32011  nmopcoi  32075  opsqrlem6  32125  hstle  32210  hst0  32213  mdsl2i  32302  superpos  32334  dmdbr5ati  32402  f1rnen  32604  resvsca  33298  pthhashvtx  35109  cvmliftphtlem  35298  topdifinffinlem  37329  finixpnum  37593  tan2h  37600  poimirlem3  37611  poimirlem4  37612  poimirlem7  37615  poimirlem16  37624  poimirlem17  37625  poimirlem19  37627  poimirlem20  37628  poimirlem24  37632  poimirlem28  37636  mblfinlem2  37646  mblfinlem4  37648  ismblfin  37649  el3v2  38207  atlatle  39307  pmaple  39749  dihglblem2N  41282  sn-ltaddneg  42436  elnnrabdioph  42789  rabren3dioph  42797  zindbi  42929  expgrowth  44318  binomcxplemnotnn0  44339  trelpss  44438  etransc  46275  mogoldbb  47780  pgrple2abl  48347  aacllem  49784