Theorem mp3an1 1450

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an1.1	⊢ 𝜑
mp3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 690	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:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7726  tfrlem9  8307  oaord1  8469  oaword2  8471  oawordeulem  8472  oa00  8477  omword1  8491  omword2  8492  omlimcl  8496  oeoelem  8516  nnaordex  8556  naddword1  8609  undom  8982  sucdom2  9117  fodomfi  9201  fodomfib  9219  dffi3  9321  unbnn3  9555  ttrcltr  9612  frmin  9645  frrlem16  9654  pwdjuen  10076  zorn2  10400  zornn0  10402  ttukey  10412  brdom7disj  10425  brdom6disj  10426  muladd11  11286  negsubdi  11420  mulneg1  11556  ltaddpos  11610  addge01  11630  reccl  11786  recid  11793  recid2  11794  div0  11812  recdiv2  11837  divdiv23zi  11877  ltmul12a  11980  lemul12a  11982  mulgt1OLD  11983  ltmulgt11  11984  gt0div  11991  ge0div  11992  lediv12a  12018  ledivp1  12027  ltdiv23i  12049  ledivp1i  12050  ltdivp1i  12051  infm3  12084  8th4div3  12344  gtndiv  12553  nn0ind  12571  xrre2  13072  2resupmax  13090  qsqueeze  13103  xmulpnf1  13176  xlemul1a  13190  ioorebas  13354  elfz0ubfz0  13535  le2sq2  14042  expubnd  14085  crreczi  14135  bccl  14229  hashbc  14360  wrdred1hash  14468  ccatlid  14493  shftfval  14977  sgnp  14997  sqreulem  15267  binom1p  15738  fallrisefac  15932  efsub  16009  efi4p  16046  sinadd  16073  cosadd  16074  demoivreALT  16110  rpnnen2lem4  16126  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  divalglem4  16307  divalglem9  16312  gcdcllem3  16412  gcdadd  16437  algcvgblem  16488  isprm3  16594  1arith2  16840  vdwap0  16888  vdwap1  16889  ipolt  18441  smndex1sgrp  18782  f1otrspeq  19326  rmodislmod  20833  cnfldneg  21302  cnflddiv  21307  cnflddivOLD  21308  cnfldmulg  21310  cnfldexp  21311  zringsub  21362  zringmulg  21363  zringsubgval  21377  remulg  21514  resubgval  21516  thlleval  21605  mplsubrglem  21911  evls1rhm  22207  iccordt  23099  bl2ioo  24678  xrsblre  24698  iccntr  24708  icccmplem3  24711  reconnlem2  24714  opnreen  24718  mpomulcn  24756  iccpnfcnv  24840  cnllycmp  24853  pcoptcl  24919  ismbl2  25426  cmmbl  25433  nulmbl  25434  unmbl  25436  voliunlem2  25450  ioombl1  25461  opnmbllem  25500  mbfima  25529  ellimc3  25778  limcflf  25780  coe1termlem  26161  dvnply2  26193  dvnply  26194  reeff1o  26355  sinperlem  26387  resinf1o  26443  logeftb  26490  logge0  26512  efopn  26565  loglesqrt  26669  logrec  26671  xrlimcnp  26876  ppinncl  27082  chtrpcl  27083  bposlem2  27194  bposlem8  27200  lgsdir2  27239  1lgs  27249  nosupno  27613  nosupbday  27615  noinfno  27628  noinfbday  27630  noetasuplem4  27646  lrrecfr  27857  sltmul  28046  ax5seglem2  28878  axcontlem2  28914  fusgrfis  29279  3cyclfrgrrn  30234  isgrpoi  30446  imsmetlem  30638  nmcvcn  30643  ipval2  30655  lnocoi  30705  nmlno0lem  30741  nmblolbii  30747  blometi  30751  blocnilem  30752  blocni  30753  ipasslem1  30779  ipasslem2  30780  ipasslem4  30782  ipasslem5  30783  ipasslem8  30785  ipblnfi  30803  ip2eqi  30804  ubthlem1  30818  htthlem  30865  h2hmetdval  30926  axhvcom-zf  30931  axhis1-zf  30942  axhis4-zf  30945  hvm1neg  30980  hvsub4  30985  hvsubass  30992  hvsubdistr2  30998  hv2times  31009  hvsubcan  31022  hvsubcan2  31023  his2sub  31040  norm-i  31077  normpyc  31094  hhip  31125  hhph  31126  norm1exi  31198  hhssabloilem  31209  hhssnv  31212  hhshsslem2  31216  hhssmetdval  31225  shscli  31265  shunssi  31316  shsleji  31318  shsidmi  31332  spanunsni  31527  h1datomi  31529  spansncvi  31600  pjss2i  31628  pjssmii  31629  pjocini  31646  homullid  31748  honegdi  31757  ho2times  31767  nmopge0  31859  nmopgt0  31860  nmfnge0  31875  lnopaddi  31919  lnopmuli  31920  lnopsubi  31922  hmopbdoptHIL  31936  nmbdoplbi  31972  nmcoplbi  31976  nmophmi  31979  lnopconi  31982  lnfnaddi  31991  lnfnsubi  31994  nmbdfnlbi  31997  nmcfnlbi  32000  lnfnconi  32003  imaelshi  32006  cnlnadjlem2  32016  cnlnadjlem7  32021  nmoptrii  32042  nmopcoi  32043  adjcoi  32048  nmopcoadji  32049  bracnlnval  32062  leopmul  32082  opsqrlem1  32088  opsqrlem6  32093  hmopidmpji  32100  sto2i  32185  strlem1  32198  atcveq0  32296  atcv0eq  32327  atomli  32330  atcvati  32334  atcvat3i  32344  cdjreui  32380  cdj1i  32381  xdiv0  32878  xdivpnfrp  32882  mhmhmeotmd  33910  rezh  33952  qqhucn  33975  blsconn  35237  cnllysconn  35238  sate0fv0  35410  prv0  35423  sinccvglem  35665  opnrebl2  36315  ptrecube  37620  poimirlem6  37626  poimirlem7  37627  poimirlem29  37649  poimirlem30  37650  opnmbllem0  37656  mblfinlem3  37659  mblfinlem4  37660  ismblfin  37661  voliunnfl  37664  ftc1anclem5  37697  ftc1anclem7  37699  ftc1anclem8  37700  ftc1anc  37701  heiborlem7  37817  rrnequiv  37835  ismrer1  37838  el3v1  38218  cnaddcom  38971  lcmineqlem1  42022  sn-ltaddpos  42446  mapco2  42708  mzpaddmpt  42734  mzpmulmpt  42735  zindbi  42939  mpaaeu  43143  tfsconcat0b  43339  eel000cT  44696  eel0TT  44697  supminfxr  45463  fmtno4prmfac  47576  pgn4cyclex  48130  aacllem  49806