Theorem mp3an1 1477

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an12  1480  mp3an1i  1483  mp3anl1  1484  mp3an  1490  mp3an2i  1495  mp3an3an  1496  onint  7788  tfrlem9  8372  oaord1  8538  oaword2  8540  oawordeulem  8541  oa00  8546  omword1  8560  omword2  8561  omlimcl  8565  oeoelem  8586  nnaordex  8626  naddword1  8680  undom  9063  sucdom2  9197  fodomfi  9282  fodomfib  9298  dffi3  9401  unbnn3  9638  ttrcltr  9695  frmin  9731  frrlem16  9740  pwdjuen  10217  zorn2  10541  zornn0  10543  ttukey  10553  brdom7disj  10567  brdom6disj  10568  muladd11  11437  negsubdi  11571  mulneg1  11707  ltaddpos  11761  addge01  11781  reccl  11936  recid  11943  recid2  11944  div0  11960  recdiv2  11985  divdiv23zi  12025  ltmul12a  12128  lemul12a  12130  ltmulgt11  12131  gt0div  12138  ge0div  12139  lediv12a  12165  ledivp1  12174  ltdiv23i  12196  ledivp1i  12197  ltdivp1i  12198  infm3  12231  8th4div3  12521  gtndiv  12731  nn0ind  12749  xrre2  13255  2resupmax  13273  qsqueeze  13286  xmulpnf1  13359  xlemul1a  13373  ioorebas  13537  elfz0ubfz0  13720  le2sq2  14232  expubnd  14275  crreczi  14325  bccl  14419  hashbc  14551  wrdred1hash  14659  ccatlid  14685  shftfval  15176  sgnp  15196  sqreulem  15480  binom1p  15953  fallrisefac  16145  efsub  16221  efi4p  16258  sinadd  16285  cosadd  16286  demoivreALT  16322  rpnnen2lem4  16338  odd2np1  16464  opoe  16486  omoe  16487  opeo  16488  omeo  16489  divalglem4  16519  divalglem9  16524  gcdcllem3  16624  gcdadd  16649  algcvgblem  16700  isprm3  16806  1arith2  17053  vdwap0  17101  vdwap1  17102  ipolt  18656  smndex1sgrp  19054  f1otrspeq  19608  rmodislmod  21152  cnfldneg  21651  cnflddiv  21655  cnfldmulg  21657  cnfldexp  21658  zringsub  21708  zringmulg  21709  zringsubgval  21723  remulg  21860  resubgval  21862  thlleval  21951  mplsubrglem  22258  evls1rhm  22587  iccordt  23479  bl2ioo  25058  xrsblre  25078  iccntr  25088  icccmplem3  25091  reconnlem2  25094  opnreen  25098  mpomulcn  25135  iccpnfcnv  25212  cnllycmp  25224  pcoptcl  25289  ismbl2  25795  cmmbl  25802  nulmbl  25803  unmbl  25805  voliunlem2  25819  ioombl1  25830  opnmbllem  25869  mbfima  25898  ellimc3  26146  limcflf  26148  coe1termlem  26524  dvnply2  26557  dvnply  26558  reeff1o  26723  sinperlem  26758  resinf1o  26813  logeftb  26860  logge0  26882  efopn  26935  loglesqrt  27038  logrec  27040  xrlimcnp  27245  ppinncl  27450  chtrpcl  27451  bposlem2  27561  bposlem8  27567  lgsdir2  27606  1lgs  27616  nosupno  27979  nosupbday  27981  noinfno  27994  noinfbday  27996  noetasuplem4  28012  lrrecfr  28248  ltmuls  28441  bdayfinbndlem1  28772  ax5seglem2  29426  axcontlem2  29462  fusgrfis  29830  3cyclfrgrrn  30806  isgrpoi  31019  imsmetlem  31211  nmcvcn  31216  ipval2  31228  lnocoi  31278  nmlno0lem  31314  nmblolbii  31320  blometi  31324  blocnilem  31325  blocni  31326  ipasslem1  31352  ipasslem2  31353  ipasslem4  31355  ipasslem5  31356  ipasslem8  31358  ipblnfi  31376  ip2eqi  31377  ubthlem1  31391  htthlem  31438  h2hmetdval  31499  axhvcom-zf  31504  axhis1-zf  31515  axhis4-zf  31518  hvm1neg  31553  hvsub4  31558  hvsubass  31565  hvsubdistr2  31571  hv2times  31582  hvsubcan  31595  hvsubcan2  31596  his2sub  31613  norm-i  31650  normpyc  31667  hhip  31698  hhph  31699  norm1exi  31771  hhssabloilem  31782  hhssnv  31785  hhshsslem2  31789  hhssmetdval  31798  shscli  31838  shunssi  31889  shsleji  31891  shsidmi  31905  spanunsni  32100  h1datomi  32102  spansncvi  32173  pjss2i  32201  pjssmii  32202  pjocini  32219  homullid  32321  honegdi  32330  ho2times  32340  nmopge0  32432  nmopgt0  32433  nmfnge0  32448  lnopaddi  32492  lnopmuli  32493  lnopsubi  32495  hmopbdoptHIL  32509  nmbdoplbi  32545  nmcoplbi  32549  nmophmi  32552  lnopconi  32555  lnfnaddi  32564  lnfnsubi  32567  nmbdfnlbi  32570  nmcfnlbi  32573  lnfnconi  32576  imaelshi  32579  cnlnadjlem2  32589  cnlnadjlem7  32594  nmoptrii  32615  nmopcoi  32616  adjcoi  32621  nmopcoadji  32622  bracnlnval  32635  leopmul  32655  opsqrlem1  32661  opsqrlem6  32666  hmopidmpji  32673  sto2i  32758  strlem1  32771  atcveq0  32869  atcv0eq  32900  atomli  32903  atcvati  32907  atcvat3i  32917  cdjreui  32953  cdj1i  32954  xdiv0  33414  xdivpnfrp  33418  mhmhmeotmd  34478  rezh  34520  qqhucn  34543  blsconn  35924  cnllysconn  35925  sate0fv0  36097  prv0  36110  sinccvglem  36352  opnrebl2  37025  ptrecube  38452  poimirlem6  38458  poimirlem7  38459  poimirlem29  38481  poimirlem30  38482  opnmbllem0  38488  mblfinlem3  38491  mblfinlem4  38492  ismblfin  38493  voliunnfl  38496  ftc1anclem5  38529  ftc1anclem7  38531  ftc1anclem8  38532  ftc1anc  38533  heiborlem7  38665  rrnequiv  38683  ismrer1  38686  el3v1  39076  preuniqval  39342  cnaddcom  39943  lcmineqlem1  42993  sn-ltaddpos  43439  mapco2  43658  mzpaddmpt  43684  mzpmulmpt  43685  zindbi  43885  mpaaeu  44089  tfsconcat0b  44285  eel000cT  45623  eel0TT  45624  supminfxr  46390  fmtno4prmfac  48573  pgn4cyclex  49140  aacllem  50855