Theorem mp3an1 1451

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 691	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  mp3an12  1454  mp3an1i  1457  mp3anl1  1458  mp3an  1464  mp3an2i  1469  mp3an3an  1470  onint  7733  tfrlem9  8313  oaord1  8475  oaword2  8477  oawordeulem  8478  oa00  8483  omword1  8497  omword2  8498  omlimcl  8502  oeoelem  8523  nnaordex  8563  naddword1  8616  undom  8992  sucdom2  9126  fodomfi  9211  fodomfib  9228  dffi3  9333  unbnn3  9569  ttrcltr  9626  frmin  9662  frrlem16  9671  pwdjuen  10093  zorn2  10417  zornn0  10419  ttukey  10429  brdom7disj  10442  brdom6disj  10443  muladd11  11305  negsubdi  11439  mulneg1  11575  ltaddpos  11629  addge01  11649  reccl  11805  recid  11812  recid2  11813  div0  11831  recdiv2  11857  divdiv23zi  11897  ltmul12a  12000  lemul12a  12002  mulgt1OLD  12003  ltmulgt11  12004  gt0div  12011  ge0div  12012  lediv12a  12038  ledivp1  12047  ltdiv23i  12069  ledivp1i  12070  ltdivp1i  12071  infm3  12104  8th4div3  12386  gtndiv  12595  nn0ind  12613  xrre2  13111  2resupmax  13129  qsqueeze  13142  xmulpnf1  13215  xlemul1a  13229  ioorebas  13393  elfz0ubfz0  13575  le2sq2  14086  expubnd  14129  crreczi  14179  bccl  14273  hashbc  14404  wrdred1hash  14512  ccatlid  14538  shftfval  15021  sgnp  15041  sqreulem  15311  binom1p  15785  fallrisefac  15979  efsub  16056  efi4p  16093  sinadd  16120  cosadd  16121  demoivreALT  16157  rpnnen2lem4  16173  odd2np1  16299  opoe  16321  omoe  16322  opeo  16323  omeo  16324  divalglem4  16354  divalglem9  16359  gcdcllem3  16459  gcdadd  16484  algcvgblem  16535  isprm3  16641  1arith2  16888  vdwap0  16936  vdwap1  16937  ipolt  18490  smndex1sgrp  18868  f1otrspeq  19411  rmodislmod  20914  cnfldneg  21367  cnflddiv  21371  cnfldmulg  21373  cnfldexp  21374  zringsub  21424  zringmulg  21425  zringsubgval  21439  remulg  21576  resubgval  21578  thlleval  21667  mplsubrglem  21971  evls1rhm  22275  iccordt  23167  bl2ioo  24745  xrsblre  24765  iccntr  24775  icccmplem3  24778  reconnlem2  24781  opnreen  24785  mpomulcn  24822  iccpnfcnv  24899  cnllycmp  24911  pcoptcl  24976  ismbl2  25482  cmmbl  25489  nulmbl  25490  unmbl  25492  voliunlem2  25506  ioombl1  25517  opnmbllem  25556  mbfima  25585  ellimc3  25834  limcflf  25836  coe1termlem  26211  dvnply2  26241  dvnply  26242  reeff1o  26400  sinperlem  26432  resinf1o  26488  logeftb  26535  logge0  26557  efopn  26610  loglesqrt  26713  logrec  26715  xrlimcnp  26920  ppinncl  27125  chtrpcl  27126  bposlem2  27236  bposlem8  27242  lgsdir2  27281  1lgs  27291  nosupno  27655  nosupbday  27657  noinfno  27670  noinfbday  27672  noetasuplem4  27688  lrrecfr  27923  ltmuls  28116  bdayfinbndlem1  28447  ax5seglem2  28986  axcontlem2  29022  fusgrfis  29387  3cyclfrgrrn  30344  isgrpoi  30557  imsmetlem  30749  nmcvcn  30754  ipval2  30766  lnocoi  30816  nmlno0lem  30852  nmblolbii  30858  blometi  30862  blocnilem  30863  blocni  30864  ipasslem1  30890  ipasslem2  30891  ipasslem4  30893  ipasslem5  30894  ipasslem8  30896  ipblnfi  30914  ip2eqi  30915  ubthlem1  30929  htthlem  30976  h2hmetdval  31037  axhvcom-zf  31042  axhis1-zf  31053  axhis4-zf  31056  hvm1neg  31091  hvsub4  31096  hvsubass  31103  hvsubdistr2  31109  hv2times  31120  hvsubcan  31133  hvsubcan2  31134  his2sub  31151  norm-i  31188  normpyc  31205  hhip  31236  hhph  31237  norm1exi  31309  hhssabloilem  31320  hhssnv  31323  hhshsslem2  31327  hhssmetdval  31336  shscli  31376  shunssi  31427  shsleji  31429  shsidmi  31443  spanunsni  31638  h1datomi  31640  spansncvi  31711  pjss2i  31739  pjssmii  31740  pjocini  31757  homullid  31859  honegdi  31868  ho2times  31878  nmopge0  31970  nmopgt0  31971  nmfnge0  31986  lnopaddi  32030  lnopmuli  32031  lnopsubi  32033  hmopbdoptHIL  32047  nmbdoplbi  32083  nmcoplbi  32087  nmophmi  32090  lnopconi  32093  lnfnaddi  32102  lnfnsubi  32105  nmbdfnlbi  32108  nmcfnlbi  32111  lnfnconi  32114  imaelshi  32117  cnlnadjlem2  32127  cnlnadjlem7  32132  nmoptrii  32153  nmopcoi  32154  adjcoi  32159  nmopcoadji  32160  bracnlnval  32173  leopmul  32193  opsqrlem1  32199  opsqrlem6  32204  hmopidmpji  32211  sto2i  32296  strlem1  32309  atcveq0  32407  atcv0eq  32438  atomli  32441  atcvati  32445  atcvat3i  32455  cdjreui  32491  cdj1i  32492  xdiv0  32976  xdivpnfrp  32980  mhmhmeotmd  34059  rezh  34101  qqhucn  34124  blsconn  35414  cnllysconn  35415  sate0fv0  35587  prv0  35600  sinccvglem  35842  opnrebl2  36491  ptrecube  37929  poimirlem6  37935  poimirlem7  37936  poimirlem29  37958  poimirlem30  37959  opnmbllem0  37965  mblfinlem3  37968  mblfinlem4  37969  ismblfin  37970  voliunnfl  37973  ftc1anclem5  38006  ftc1anclem7  38008  ftc1anclem8  38009  ftc1anc  38010  heiborlem7  38126  rrnequiv  38144  ismrer1  38147  el3v1  38539  preuniqval  38805  cnaddcom  39406  lcmineqlem1  42456  sn-ltaddpos  42886  mapco2  43135  mzpaddmpt  43161  mzpmulmpt  43162  zindbi  43362  mpaaeu  43566  tfsconcat0b  43762  eel000cT  45117  eel0TT  45118  supminfxr  45880  fmtno4prmfac  48023  pgn4cyclex  48590  aacllem  50264