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  3572  tz7.7  6383  ordin  6387  onfr  6396  fprresex  8314  wfrlem14OLD  8341  wfrlem17OLD  8344  tfrlem11  8407  phplem2  9224  epfrs  9750  zorng  10523  tsk2  10784  tskcard  10800  gruina  10837  muladd11  11410  00id  11415  ltaddneg  11456  negsub  11536  subneg  11537  muleqadd  11886  diveq0  11911  diveq1  11931  conjmul  11963  recp1lt1  12145  nnsub  12289  addltmul  12482  nnunb  12502  zltp1le  12647  gtndiv  12675  eluzp1m1  12883  zbtwnre  12967  rebtwnz  12968  xnn0le2is012  13267  supxrbnd  13349  divelunit  13516  fznatpl1  13600  flbi2  13839  fldiv  13882  modid  13918  modm1p1mod0  13945  fzen2  13992  nn0ennn  14002  seqshft2  14051  seqf1olem1  14064  ser1const  14081  sq01  14248  expnbnd  14255  faclbnd3  14315  faclbnd5  14321  hashunsng  14415  hashunsngx  14416  hashxplem  14456  ccatrid  14610  ccats1val1  14649  ccat2s1fst  14662  sgnn  15118  01sqrexlem2  15267  01sqrexlem7  15272  leabs  15323  abs2dif  15356  cvgrat  15904  cos2t  16201  sin01gt0  16213  cos01gt0  16214  demoivre  16223  demoivreALT  16224  rpnnen2lem5  16241  rpnnen2lem12  16248  omeo  16390  gcd0id  16543  sqgcd  16586  expgcd  16587  isprm3  16707  eulerthlem2  16806  pczpre  16872  pcrec  16883  ressress  17273  mulgm1  19082  unitgrpid  20350  mdet0pr  22535  m2detleib  22574  cmpcov2  23333  ufileu  23862  tgpconncompeqg  24055  itg2ge0  25693  mdegldg  26028  abssinper  26487  ppiub  27172  chtub  27180  bposlem2  27253  lgs1  27309  cofcutr  27889  addsbday  27981  negsbdaylem  28019  precsexlem10  28175  onscutlt  28222  n0sbday  28301  bdayn0p1  28315  eucliddivs  28322  nnzs  28331  zzs12  28396  remulscllem1  28408  colinearalglem4  28893  axsegconlem1  28901  axpaschlem  28924  axcontlem2  28949  axcontlem4  28951  axcontlem7  28954  axcontlem8  28955  funvtxval  29002  funiedgval  29003  vc0  30560  vcm  30562  nvmval2  30629  nvmf  30631  nvmdi  30634  nvnegneg  30635  nvpncan2  30639  nvaddsub4  30643  nvm1  30651  nvdif  30652  nvpi  30653  nvz0  30654  nvmtri  30657  nvabs  30658  nvge0  30659  imsmetlem  30676  4ipval2  30694  ipval3  30695  ipidsq  30696  dipcj  30700  sspmval  30719  ipasslem1  30817  ipasslem2  30818  dipsubdir  30834  hvsubdistr1  31035  shsubcl  31206  shsel3  31301  shunssi  31354  hosubdi  31794  lnopmi  31986  nmophmi  32017  nmopcoi  32081  opsqrlem6  32131  hstle  32216  hst0  32219  mdsl2i  32308  superpos  32340  dmdbr5ati  32408  f1rnen  32612  resvsca  33353  pthhashvtx  35155  cvmliftphtlem  35344  topdifinffinlem  37370  finixpnum  37634  tan2h  37641  poimirlem3  37652  poimirlem4  37653  poimirlem7  37656  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem24  37673  poimirlem28  37677  mblfinlem2  37687  mblfinlem4  37689  ismblfin  37690  el3v2  38248  atlatle  39343  pmaple  39785  dihglblem2N  41318  sn-ltaddneg  42460  elnnrabdioph  42805  rabren3dioph  42813  zindbi  42945  expgrowth  44334  binomcxplemnotnn0  44355  trelpss  44454  etransc  46292  mogoldbb  47779  pgrple2abl  48320  aacllem  49645