Theorem mp3an1 1403

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  mp3an12  1406  mp3an1i  1409  mp3anl1  1410  mp3an  1416  mp3an2i  1421  mp3an3an  1422  onint  6887  wfrlem12  7313  wfrlem17  7318  tfrlem9  7368  oaord1  7518  oaword2  7520  oawordeulem  7521  oa00  7526  omword1  7540  omword2  7541  omlimcl  7545  oeoelem  7565  nnaordex  7605  enp1i  8080  unfilem2  8110  dffi3  8220  unbnn3  8439  pwcdaen  8890  ackbij1b  8944  zorn2  9211  zornn0  9213  ttukey  9223  brdom7disj  9234  brdom6disj  9235  wunex2  9439  muladd11  10085  00id  10090  mul02  10093  negsubdi  10216  mulneg1  10345  ltaddpos  10397  addge01  10417  reccl  10571  recid  10578  recid2  10579  recdiv2  10617  divdiv23zi  10657  ltmul12a  10758  lemul12a  10760  mulgt1  10761  ltmulgt11  10762  gt0div  10768  ge0div  10769  lediv12a  10795  ledivp1  10804  ltdiv23i  10827  ledivp1i  10828  ltdivp1i  10829  infm3  10861  nngt1ne1  10924  8th4div3  11129  gtndiv  11330  nn0ind  11348  fnn0ind  11352  supminf  11651  xrre2  11875  2resupmax  11893  qsqueeze  11906  xmulpnf1  11976  xlemul1a  11990  xrub  12014  ioorebas  12146  elfz0ubfz0  12312  expubnd  12783  le2sq2  12801  crreczi  12851  bernneq  12852  faclbnd5  12947  faclbnd6  12948  bccl  12971  hashbc  13094  ccatlid  13222  shftfval  13658  sgnp  13678  mulre  13709  sqrlem4  13834  sqrlem7  13837  sqreulem  13947  binom1p  14402  0.999...OLD  14452  fallrisefac  14595  bpoly3  14628  efsub  14669  efi4p  14706  sinadd  14733  cosadd  14734  cos2t  14747  cos2tsin  14748  sin01gt0  14759  cos01gt0  14760  absefib  14767  efieq1re  14768  demoivreALT  14770  rpnnen2lem4  14785  odd2np1  14903  opoe  14925  omoe  14926  opeo  14927  omeo  14928  divalglem0  14954  divalglem4  14957  divalglem9  14962  gcdcllem3  15061  gcdn0gt0  15077  gcdadd  15085  gcdmultiple  15107  algcvgblem  15128  algcvga  15130  isprm3  15234  divgcdodd  15260  coprm  15261  pythagtriplem4  15362  pythagtriplem11  15368  pythagtriplem12  15369  pythagtriplem13  15370  pythagtriplem14  15371  infpn2  15455  1arith2  15470  vdwap0  15518  vdwap1  15519  ipolt  16982  gsumval2a  17102  f1otrspeq  17690  mplsubrglem  19260  evls1rhm  19508  cnfldneg  19591  cnflddiv  19595  cnfldmulg  19597  cnfldexp  19598  zringmulg  19645  remulg  19772  resubgval  19774  thlleval  19861  frlmsslsp  19954  neiptoptop  20745  iccordt  20828  qustgplem  21734  bl2ioo  22403  ioo2blex  22405  blssioo  22406  tgioo  22407  xrsblre  22422  iccntr  22432  icccmplem3  22435  reconnlem2  22438  opnreen  22442  iccpnfcnv  22551  cnllycmp  22563  pcoptcl  22629  ovolmge0  23052  ovolctb2  23067  ismbl2  23102  cmmbl  23109  nulmbl  23110  unmbl  23112  voliunlem1  23125  voliunlem2  23126  ioombl1  23137  opnmbllem  23175  mbfima  23205  i1fsub  23281  itg1sub  23282  ellimc3  23449  limcflf  23451  dvcnvre  23586  coe1termlem  23818  dgrsub  23832  dvnply2  23846  dvnply  23847  reeff1o  24005  sinperlem  24036  sincosq1eq  24068  resinf1o  24086  logeftb  24134  logge0  24155  logdivlti  24170  efopn  24204  logtayl2  24208  loglesqrt  24299  logrec  24301  xrlimcnp  24495  ppinncl  24700  chtrpcl  24701  bposlem2  24810  bposlem8  24816  lgsdir2  24855  1lgs  24865  brbtwn2  25585  colinearalglem4  25589  ax5seglem1  25608  ax5seglem2  25609  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  iswlkg  26052  redwlklem  26135  0vgrargra  26464  isgrpoi  26736  imsmetlem  26929  nmcvcn  26934  ipval2  26946  lnocoi  26996  nmlno0lem  27032  nmblolbii  27038  blometi  27042  blocnilem  27043  blocni  27044  ipasslem1  27070  ipasslem2  27071  ipasslem4  27073  ipasslem5  27074  ipasslem8  27076  ipblnfi  27095  ip2eqi  27096  ubthlem1  27110  htthlem  27158  h2hmetdval  27219  axhvcom-zf  27224  axhis1-zf  27235  axhis4-zf  27238  hvm1neg  27273  hvsub4  27278  hvsubass  27285  hvsubdistr2  27291  hv2times  27302  hvsubcan  27315  hvsubcan2  27316  his2sub  27333  norm-i  27370  normpyc  27387  hhip  27418  hhph  27419  norm1exi  27491  hhssabloilem  27502  hhssnv  27505  hhshsslem2  27509  hhssmetdval  27519  shscli  27560  shunssi  27611  shsleji  27613  shsidmi  27627  spanunsni  27822  h1datomi  27824  spansncvi  27895  pjss2i  27923  pjssmii  27924  pjocini  27941  homulid2  28043  honegdi  28052  ho2times  28062  nmopge0  28154  nmopgt0  28155  nmfnge0  28170  lnopaddi  28214  lnopmuli  28215  lnopsubi  28217  hmopbdoptHIL  28231  nmbdoplbi  28267  nmcoplbi  28271  nmophmi  28274  lnopconi  28277  lnfnaddi  28286  lnfnsubi  28289  nmbdfnlbi  28292  nmcfnlbi  28295  lnfnconi  28298  imaelshi  28301  cnlnadjlem2  28311  cnlnadjlem7  28316  nmoptrii  28337  nmopcoi  28338  adjcoi  28343  nmopcoadji  28344  bracnlnval  28357  leopmul  28377  opsqrlem1  28383  opsqrlem6  28388  hmopidmpji  28395  sto2i  28480  strlem1  28493  atcveq0  28591  atcv0eq  28622  atomli  28625  atcvati  28629  atcvat3i  28639  cdjreui  28675  cdj1i  28676  xdiv0  28968  xdivpnfrp  28972  mhmhmeotmd  29301  rezh  29343  qqhucn  29364  blscon  30480  cnllyscon  30481  sinccvglem  30820  frrlem11  31036  nobndlem8  31098  opnrebl2  31486  ptrecube  32579  poimirlem6  32585  poimirlem7  32586  poimirlem29  32608  poimirlem30  32609  opnmbllem0  32615  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  voliunnfl  32623  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  heiborlem7  32786  rrnequiv  32804  ismrer1  32807  cnaddcom  33277  mapco2  36296  mzpaddmpt  36322  mzpmulmpt  36323  zindbi  36529  mpaaeu  36739  eel000cT  37949  eel0TT  37950  fmtno4prmfac  40022  wrdred1hash  40241  fusgrfis  40549  3cyclfrgrrn  41456  zringsubgval  41977  aacllem  42356