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  7804  tfrlem9  8393  oaord1  8559  oaword2  8561  oawordeulem  8562  oa00  8567  omword1  8581  omword2  8582  omlimcl  8586  oeoelem  8607  nnaordex  8647  naddword1  8701  undom  9084  sucdom2  9218  fodomfi  9304  fodomfib  9320  dffi3  9423  unbnn3  9660  ttrcltr  9717  frmin  9753  frrlem16  9762  pwdjuen  10260  zorn2  10584  zornn0  10586  ttukey  10596  brdom7disj  10610  brdom6disj  10611  muladd11  11480  negsubdi  11614  mulneg1  11752  ltaddpos  11806  addge01  11826  reccl  11981  recid  11988  recid2  11989  div0  12005  recdiv2  12030  divdiv23zi  12070  ltmul12a  12173  lemul12a  12175  ltmulgt11  12176  gt0div  12183  ge0div  12184  lediv12a  12210  ledivp1  12219  ltdiv23i  12241  ledivp1i  12242  ltdivp1i  12243  infm3  12276  8th4div3  12566  gtndiv  12776  nn0ind  12794  xrre2  13300  2resupmax  13318  qsqueeze  13331  xmulpnf1  13404  xlemul1a  13418  ioorebas  13582  elfz0ubfz0  13766  le2sq2  14278  expubnd  14321  crreczi  14372  bccl  14466  hashbc  14598  wrdred1hash  14706  ccatlid  14732  shftfval  15223  sgnp  15243  sqreulem  15527  binom1p  16000  fallrisefac  16192  efsub  16268  efi4p  16305  sinadd  16332  cosadd  16333  demoivreALT  16369  rpnnen2lem4  16385  odd2np1  16511  opoe  16533  omoe  16534  opeo  16535  omeo  16536  divalglem4  16566  divalglem9  16571  gcdcllem3  16671  gcdadd  16698  algcvgblem  16752  isprm3  16858  1arith2  17106  vdwap0  17154  vdwap1  17155  ipolt  18709  smndex1sgrp  19107  f1otrspeq  19661  rmodislmod  21205  cnfldneg  21704  cnflddiv  21708  cnfldmulg  21710  cnfldexp  21711  zringsub  21761  zringmulg  21762  zringsubgval  21776  remulg  21913  resubgval  21915  thlleval  22004  mplsubrglem  22311  evls1rhm  22640  iccordt  23532  bl2ioo  25111  xrsblre  25131  iccntr  25141  icccmplem3  25144  reconnlem2  25147  opnreen  25151  mpomulcn  25188  iccpnfcnv  25265  cnllycmp  25277  pcoptcl  25342  ismbl2  25848  cmmbl  25855  nulmbl  25856  unmbl  25858  voliunlem2  25872  ioombl1  25883  opnmbllem  25922  mbfima  25951  ellimc3  26199  limcflf  26201  coe1termlem  26577  dvnply2  26608  dvnply  26609  reeff1o  26774  sinperlem  26809  resinf1o  26864  logeftb  26911  logge0  26933  efopn  26986  loglesqrt  27089  logrec  27091  xrlimcnp  27296  ppinncl  27501  chtrpcl  27502  bposlem2  27612  bposlem8  27618  lgsdir2  27657  1lgs  27667  nosupno  28060  nosupbday  28062  noinfno  28075  noinfbday  28077  noetasuplem4  28093  lrrecfr  28329  ltmuls  28522  bdayfinbndlem1  28853  ax5seglem2  29507  axcontlem2  29543  fusgrfis  29911  3cyclfrgrrn  30887  isgrpoi  31100  imsmetlem  31292  nmcvcn  31297  ipval2  31309  lnocoi  31359  nmlno0lem  31395  nmblolbii  31401  blometi  31405  blocnilem  31406  blocni  31407  ipasslem1  31433  ipasslem2  31434  ipasslem4  31436  ipasslem5  31437  ipasslem8  31439  ipblnfi  31457  ip2eqi  31458  ubthlem1  31472  htthlem  31519  h2hmetdval  31580  axhvcom-zf  31585  axhis1-zf  31596  axhis4-zf  31599  hvm1neg  31634  hvsub4  31639  hvsubass  31646  hvsubdistr2  31652  hv2times  31663  hvsubcan  31676  hvsubcan2  31677  his2sub  31694  norm-i  31731  normpyc  31748  hhip  31779  hhph  31780  norm1exi  31852  hhssabloilem  31863  hhssnv  31866  hhshsslem2  31870  hhssmetdval  31879  shscli  31919  shunssi  31970  shsleji  31972  shsidmi  31986  spanunsni  32181  h1datomi  32183  spansncvi  32254  pjss2i  32282  pjssmii  32283  pjocini  32300  homullid  32402  honegdi  32411  ho2times  32421  nmopge0  32513  nmopgt0  32514  nmfnge0  32529  lnopaddi  32573  lnopmuli  32574  lnopsubi  32576  hmopbdoptHIL  32590  nmbdoplbi  32626  nmcoplbi  32630  nmophmi  32633  lnopconi  32636  lnfnaddi  32645  lnfnsubi  32648  nmbdfnlbi  32651  nmcfnlbi  32654  lnfnconi  32657  imaelshi  32660  cnlnadjlem2  32670  cnlnadjlem7  32675  nmoptrii  32696  nmopcoi  32697  adjcoi  32702  nmopcoadji  32703  bracnlnval  32716  leopmul  32736  opsqrlem1  32742  opsqrlem6  32747  hmopidmpji  32754  sto2i  32839  strlem1  32852  atcveq0  32950  atcv0eq  32981  atomli  32984  atcvati  32988  atcvat3i  32998  cdjreui  33034  cdj1i  33035  xdiv0  33495  xdivpnfrp  33499  mhmhmeotmd  34559  rezh  34601  qqhucn  34624  blsconn  36009  cnllysconn  36010  sate0fv0  36182  prv0  36195  sinccvglem  36437  opnrebl2  37109  ptrecube  38539  poimirlem6  38545  poimirlem7  38546  poimirlem29  38568  poimirlem30  38569  opnmbllem0  38575  mblfinlem3  38578  mblfinlem4  38579  ismblfin  38580  voliunnfl  38583  ftc1anclem5  38616  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  heiborlem7  38752  rrnequiv  38770  ismrer1  38773  el3v1  39163  preuniqval  39429  cnaddcom  40030  lcmineqlem1  43080  sn-ltaddpos  43518  mapco2  43726  mzpaddmpt  43752  mzpmulmpt  43753  zindbi  43953  mpaaeu  44152  tfsconcat0b  44348  eel000cT  45685  eel0TT  45686  supminfxr  46474  fmtno4prmfac  48657  pgn4cyclex  49224  aacllem  50939