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 698	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  mp3anl2  1455  tz7.7  6314  ordin  6318  onfr  6327  fprresex  8174  wfrlem14OLD  8201  wfrlem17OLD  8204  tfrlem11  8267  phplem2  9051  epfrs  9566  zorng  10339  tsk2  10600  tskcard  10616  gruina  10653  muladd11  11224  00id  11229  ltaddneg  11269  negsub  11348  subneg  11349  muleqadd  11698  diveq1  11745  conjmul  11771  recp1lt1  11952  nnsub  12096  addltmul  12288  nnunb  12308  zltp1le  12449  gtndiv  12476  eluzp1m1  12687  zbtwnre  12765  rebtwnz  12766  xnn0le2is012  13059  supxrbnd  13141  divelunit  13305  fznatpl1  13389  flbi2  13616  fldiv  13659  modid  13695  modm1p1mod0  13721  fzen2  13768  nn0ennn  13778  seqshft2  13828  seqf1olem1  13841  ser1const  13858  sq01  14019  expnbnd  14026  faclbnd3  14085  faclbnd5  14091  hashunsng  14185  hashunsngx  14186  hashxplem  14226  ccatrid  14369  ccats1val1  14408  ccat2s1fst  14427  sgnn  14881  sqrlem2  15031  sqrlem7  15036  leabs  15087  abs2dif  15120  cvgrat  15671  cos2t  15963  sin01gt0  15975  cos01gt0  15976  demoivre  15985  demoivreALT  15986  rpnnen2lem5  16003  rpnnen2lem12  16010  omeo  16151  gcd0id  16302  sqgcd  16344  isprm3  16462  eulerthlem2  16557  pczpre  16622  pcrec  16633  ressress  17032  mulgm1  18797  unitgrpid  19983  mdet0pr  21821  m2detleib  21860  cmpcov2  22621  ufileu  23150  tgpconncompeqg  23343  itg2ge0  24980  mdegldg  25311  abssinper  25757  ppiub  26432  chtub  26440  bposlem2  26513  lgs1  26569  colinearalglem4  27410  axsegconlem1  27418  axpaschlem  27441  axcontlem2  27466  axcontlem4  27468  axcontlem7  27471  axcontlem8  27472  funvtxval  27521  funiedgval  27522  vc0  29068  vcm  29070  nvmval2  29137  nvmf  29139  nvmdi  29142  nvnegneg  29143  nvpncan2  29147  nvaddsub4  29151  nvm1  29159  nvdif  29160  nvpi  29161  nvz0  29162  nvmtri  29165  nvabs  29166  nvge0  29167  imsmetlem  29184  4ipval2  29202  ipval3  29203  ipidsq  29204  dipcj  29208  sspmval  29227  ipasslem1  29325  ipasslem2  29326  dipsubdir  29342  hvsubdistr1  29543  shsubcl  29714  shsel3  29809  shunssi  29862  hosubdi  30302  lnopmi  30494  nmophmi  30525  nmopcoi  30589  opsqrlem6  30639  hstle  30724  hst0  30727  mdsl2i  30816  superpos  30848  dmdbr5ati  30916  f1rnen  31095  resvsca  31663  pthhashvtx  33224  cvmliftphtlem  33414  cofcutr  34162  topdifinffinlem  35595  finixpnum  35839  tan2h  35846  poimirlem3  35857  poimirlem4  35858  poimirlem7  35861  poimirlem16  35870  poimirlem17  35871  poimirlem19  35873  poimirlem20  35874  poimirlem24  35878  poimirlem28  35882  mblfinlem2  35892  mblfinlem4  35894  ismblfin  35895  el3v2  36455  atlatle  37559  pmaple  38001  dihglblem2N  39534  expgcd  40555  elnnrabdioph  40850  rabren3dioph  40858  zindbi  40990  expgrowth  42192  binomcxplemnotnn0  42213  trelpss  42312  etransc  44079  mogoldbb  45507  pgrple2abl  45971  aacllem  46775