Theorem mp3an2 1458

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 1125	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 708	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  mp3anl2  1465  vtoclegft  3528  tz7.7  6339  ordin  6343  onfr  6352  fprresex  8253  tfrlem11  8321  phplem2  9133  epfrs  9647  zorng  10422  tsk2  10684  tskcard  10700  gruina  10737  muladd11  11312  00id  11317  ltaddneg  11358  negsub  11438  subneg  11439  muleqadd  11790  diveq0  11814  diveq1  11834  conjmul  11867  recp1lt1  12049  nnsub  12216  addltmul  12408  nnunb  12428  zltp1le  12572  gtndiv  12601  eluzp1m1  12809  zbtwnre  12891  rebtwnz  12892  xnn0le2is012  13193  supxrbnd  13275  divelunit  13442  fznatpl1  13527  flbi2  13771  fldiv  13814  modid  13850  modm1p1mod0  13879  fzen2  13926  nn0ennn  13936  seqshft2  13985  seqf1olem1  13998  ser1const  14015  sq01  14182  expnbnd  14189  faclbnd3  14249  faclbnd5  14255  hashunsng  14349  hashunsngx  14350  hashxplem  14390  ccatrid  14545  ccats1val1  14584  ccat2s1fst  14597  sgnn  15051  01sqrexlem2  15200  01sqrexlem7  15205  leabs  15256  abs2dif  15290  cvgrat  15843  cos2t  16140  sin01gt0  16152  cos01gt0  16153  demoivre  16162  demoivreALT  16163  rpnnen2lem5  16180  rpnnen2lem12  16187  omeo  16330  gcd0id  16483  sqgcd  16526  expgcd  16527  isprm3  16647  eulerthlem2  16747  pczpre  16813  pcrec  16824  ressress  17212  mulgm1  19065  unitgrpid  20359  mdet0pr  22578  m2detleib  22617  cmpcov2  23376  ufileu  23905  tgpconncompeqg  24098  itg2ge0  25723  mdegldg  26052  abssinper  26506  ppiub  27188  chtub  27196  bposlem2  27269  lgs1  27325  cofcutr  27936  addbday  28030  negbdaylem  28068  precsexlem10  28228  oncutlt  28276  n0bday  28364  bdayn0p1  28381  eucliddivs  28388  nnzs  28398  bdaypw2n0bndlem  28475  zz12s  28487  remulscllem1  28512  colinearalglem4  28998  axsegconlem1  29006  axpaschlem  29029  axcontlem2  29054  axcontlem4  29056  axcontlem7  29059  axcontlem8  29060  funvtxval  29107  funiedgval  29108  vc0  30665  vcm  30667  nvmval2  30734  nvmf  30736  nvmdi  30739  nvnegneg  30740  nvpncan2  30744  nvaddsub4  30748  nvm1  30756  nvdif  30757  nvpi  30758  nvz0  30759  nvmtri  30762  nvabs  30763  nvge0  30764  imsmetlem  30781  4ipval2  30799  ipval3  30800  ipidsq  30801  dipcj  30805  sspmval  30824  ipasslem1  30922  ipasslem2  30923  dipsubdir  30939  hvsubdistr1  31140  shsubcl  31311  shsel3  31406  shunssi  31459  hosubdi  31899  lnopmi  32091  nmophmi  32122  nmopcoi  32186  opsqrlem6  32236  hstle  32321  hst0  32324  mdsl2i  32413  superpos  32445  dmdbr5ati  32513  f1rnen  32722  resvsca  33417  noinfepfnregs  35326  pthhashvtx  35369  cvmliftphtlem  35558  topdifinffinlem  37722  finixpnum  37985  tan2h  37992  poimirlem3  38003  poimirlem4  38004  poimirlem7  38007  poimirlem16  38016  poimirlem17  38017  poimirlem19  38019  poimirlem20  38020  poimirlem24  38024  poimirlem28  38028  mblfinlem2  38038  mblfinlem4  38040  ismblfin  38041  el3v2  38611  atlatle  39825  pmaple  40266  dihglblem2N  41799  sn-ltaddneg  42957  elnnrabdioph  43265  rabren3dioph  43273  zindbi  43404  expgrowth  44792  binomcxplemnotnn0  44813  trelpss  44911  etransc  46738  mogoldbb  48288  pgrple2abl  48868  aacllem  50303