Theorem mp3an1 1449

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 689	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

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

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

This theorem is referenced by:  mp3an12  1452  mp3an1i  1455  mp3anl1  1456  mp3an  1462  mp3an2i  1467  mp3an3an  1468  onint  7778  wfrlem12OLD  8320  tfrlem9  8385  oaord1  8551  oaword2  8553  oawordeulem  8554  oa00  8559  omword1  8573  omword2  8574  omlimcl  8578  oeoelem  8598  nnaordex  8638  naddword1  8690  undom  9059  rexdif1enOLD  9159  sucdom2  9206  enp1iOLD  9280  dffi3  9426  unbnn3  9654  ttrcltr  9711  frmin  9744  frrlem16  9753  pwdjuen  10176  zorn2  10501  zornn0  10503  ttukey  10513  brdom7disj  10526  brdom6disj  10527  muladd11  11384  negsubdi  11516  mulneg1  11650  ltaddpos  11704  addge01  11724  reccl  11879  recid  11886  recid2  11887  recdiv2  11927  divdiv23zi  11967  ltmul12a  12070  lemul12a  12072  mulgt1  12073  ltmulgt11  12074  gt0div  12080  ge0div  12081  lediv12a  12107  ledivp1  12116  ltdiv23i  12138  ledivp1i  12139  ltdivp1i  12140  infm3  12173  8th4div3  12432  gtndiv  12639  nn0ind  12657  xrre2  13149  2resupmax  13167  qsqueeze  13180  xmulpnf1  13253  xlemul1a  13267  ioorebas  13428  elfz0ubfz0  13605  le2sq2  14100  expubnd  14142  crreczi  14191  bccl  14282  hashbc  14412  wrdred1hash  14511  ccatlid  14536  shftfval  15017  sgnp  15037  sqreulem  15306  binom1p  15777  fallrisefac  15969  efsub  16043  efi4p  16080  sinadd  16107  cosadd  16108  demoivreALT  16144  rpnnen2lem4  16160  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  divalglem4  16339  divalglem9  16344  gcdcllem3  16442  gcdadd  16467  algcvgblem  16514  isprm3  16620  1arith2  16861  vdwap0  16909  vdwap1  16910  ipolt  18488  smndex1sgrp  18789  f1otrspeq  19315  rmodislmod  20540  rmodislmodOLD  20541  cnfldneg  20971  cnflddiv  20975  cnfldmulg  20977  cnfldexp  20978  zringsub  21025  zringmulg  21026  zringsubgval  21040  remulg  21160  resubgval  21162  thlleval  21253  mplsubrglem  21563  evls1rhm  21841  iccordt  22718  bl2ioo  24308  xrsblre  24327  iccntr  24337  icccmplem3  24340  reconnlem2  24343  opnreen  24347  iccpnfcnv  24460  cnllycmp  24472  pcoptcl  24537  ismbl2  25044  cmmbl  25051  nulmbl  25052  unmbl  25054  voliunlem2  25068  ioombl1  25079  opnmbllem  25118  mbfima  25147  ellimc3  25396  limcflf  25398  coe1termlem  25772  dvnply2  25800  dvnply  25801  reeff1o  25959  sinperlem  25990  resinf1o  26045  logeftb  26092  logge0  26113  efopn  26166  loglesqrt  26266  logrec  26268  xrlimcnp  26473  ppinncl  26678  chtrpcl  26679  bposlem2  26788  bposlem8  26794  lgsdir2  26833  1lgs  26843  nosupno  27206  nosupbday  27208  noinfno  27221  noinfbday  27223  noetasuplem4  27239  lrrecfr  27429  sltmul  27595  ax5seglem2  28218  axcontlem2  28254  fusgrfis  28618  3cyclfrgrrn  29570  isgrpoi  29782  imsmetlem  29974  nmcvcn  29979  ipval2  29991  lnocoi  30041  nmlno0lem  30077  nmblolbii  30083  blometi  30087  blocnilem  30088  blocni  30089  ipasslem1  30115  ipasslem2  30116  ipasslem4  30118  ipasslem5  30119  ipasslem8  30121  ipblnfi  30139  ip2eqi  30140  ubthlem1  30154  htthlem  30201  h2hmetdval  30262  axhvcom-zf  30267  axhis1-zf  30278  axhis4-zf  30281  hvm1neg  30316  hvsub4  30321  hvsubass  30328  hvsubdistr2  30334  hv2times  30345  hvsubcan  30358  hvsubcan2  30359  his2sub  30376  norm-i  30413  normpyc  30430  hhip  30461  hhph  30462  norm1exi  30534  hhssabloilem  30545  hhssnv  30548  hhshsslem2  30552  hhssmetdval  30561  shscli  30601  shunssi  30652  shsleji  30654  shsidmi  30668  spanunsni  30863  h1datomi  30865  spansncvi  30936  pjss2i  30964  pjssmii  30965  pjocini  30982  homullid  31084  honegdi  31093  ho2times  31103  nmopge0  31195  nmopgt0  31196  nmfnge0  31211  lnopaddi  31255  lnopmuli  31256  lnopsubi  31258  hmopbdoptHIL  31272  nmbdoplbi  31308  nmcoplbi  31312  nmophmi  31315  lnopconi  31318  lnfnaddi  31327  lnfnsubi  31330  nmbdfnlbi  31333  nmcfnlbi  31336  lnfnconi  31339  imaelshi  31342  cnlnadjlem2  31352  cnlnadjlem7  31357  nmoptrii  31378  nmopcoi  31379  adjcoi  31384  nmopcoadji  31385  bracnlnval  31398  leopmul  31418  opsqrlem1  31424  opsqrlem6  31429  hmopidmpji  31436  sto2i  31521  strlem1  31534  atcveq0  31632  atcv0eq  31663  atomli  31666  atcvati  31670  atcvat3i  31680  cdjreui  31716  cdj1i  31717  xdiv0  32126  xdivpnfrp  32130  mhmhmeotmd  32938  rezh  32982  qqhucn  33003  blsconn  34266  cnllysconn  34267  sate0fv0  34439  prv0  34452  sinccvglem  34688  mpomulcn  35193  opnrebl2  35254  ptrecube  36536  poimirlem6  36542  poimirlem7  36543  poimirlem29  36565  poimirlem30  36566  opnmbllem0  36572  mblfinlem3  36575  mblfinlem4  36576  ismblfin  36577  voliunnfl  36580  ftc1anclem5  36613  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  heiborlem7  36733  rrnequiv  36751  ismrer1  36754  el3v1  37135  cnaddcom  37890  lcmineqlem1  40942  2xp3dxp2ge1d  41070  sn-ltaddpos  41362  mapco2  41501  mzpaddmpt  41527  mzpmulmpt  41528  zindbi  41733  mpaaeu  41940  tfsconcat0b  42144  eel000cT  43512  eel0TT  43513  supminfxr  44222  fmtno4prmfac  46288  aacllem  47896