Theorem mp3an1 1474

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3an12  1477  mp3an1i  1480  mp3anl1  1481  mp3an  1487  mp3an2i  1492  mp3an3an  1493  onint  7789  tfrlem9  8372  oaord1  8536  oaword2  8538  oawordeulem  8539  oa00  8544  omword1  8558  omword2  8559  omlimcl  8563  oeoelem  8584  nnaordex  8624  naddword1  8678  undom  9053  sucdom2  9187  fodomfi  9272  fodomfib  9288  dffi3  9391  unbnn3  9628  ttrcltr  9685  frmin  9721  frrlem16  9730  pwdjuen  10165  zorn2  10490  zornn0  10492  ttukey  10502  brdom7disj  10515  brdom6disj  10516  muladd11  11380  negsubdi  11514  mulneg1  11650  ltaddpos  11704  addge01  11724  reccl  11879  recid  11886  recid2  11887  div0  11903  recdiv2  11928  divdiv23zi  11968  ltmul12a  12071  lemul12a  12073  ltmulgt11  12074  gt0div  12081  ge0div  12082  lediv12a  12108  ledivp1  12117  ltdiv23i  12139  ledivp1i  12140  ltdivp1i  12141  infm3  12174  8th4div3  12464  gtndiv  12673  nn0ind  12691  xrre2  13196  2resupmax  13214  qsqueeze  13227  xmulpnf1  13300  xlemul1a  13314  ioorebas  13478  elfz0ubfz0  13660  le2sq2  14171  expubnd  14214  crreczi  14264  bccl  14358  hashbc  14490  wrdred1hash  14598  ccatlid  14624  shftfval  15107  sgnp  15127  sqreulem  15411  binom1p  15885  fallrisefac  16079  efsub  16156  efi4p  16193  sinadd  16220  cosadd  16221  demoivreALT  16257  rpnnen2lem4  16273  odd2np1  16399  opoe  16421  omoe  16422  opeo  16423  omeo  16424  divalglem4  16454  divalglem9  16459  gcdcllem3  16559  gcdadd  16584  algcvgblem  16635  isprm3  16741  1arith2  16988  vdwap0  17036  vdwap1  17037  ipolt  18591  smndex1sgrp  18970  f1otrspeq  19517  rmodislmod  21029  cnfldneg  21517  cnflddiv  21521  cnfldmulg  21523  cnfldexp  21524  zringsub  21574  zringmulg  21575  zringsubgval  21589  remulg  21726  resubgval  21728  thlleval  21817  mplsubrglem  22122  evls1rhm  22451  iccordt  23340  bl2ioo  24918  xrsblre  24938  iccntr  24948  icccmplem3  24951  reconnlem2  24954  opnreen  24958  mpomulcn  24995  iccpnfcnv  25072  cnllycmp  25084  pcoptcl  25149  ismbl2  25655  cmmbl  25662  nulmbl  25663  unmbl  25665  voliunlem2  25679  ioombl1  25690  opnmbllem  25729  mbfima  25758  ellimc3  26007  limcflf  26009  coe1termlem  26384  dvnply2  26417  dvnply  26418  reeff1o  26576  sinperlem  26611  resinf1o  26667  logeftb  26714  logge0  26736  efopn  26789  loglesqrt  26892  logrec  26894  xrlimcnp  27099  ppinncl  27304  chtrpcl  27305  bposlem2  27415  bposlem8  27421  lgsdir2  27460  1lgs  27470  nosupno  27833  nosupbday  27835  noinfno  27848  noinfbday  27850  noetasuplem4  27866  lrrecfr  28102  ltmuls  28295  bdayfinbndlem1  28626  ax5seglem2  29220  axcontlem2  29256  fusgrfis  29621  3cyclfrgrrn  30578  isgrpoi  30791  imsmetlem  30983  nmcvcn  30988  ipval2  31000  lnocoi  31050  nmlno0lem  31086  nmblolbii  31092  blometi  31096  blocnilem  31097  blocni  31098  ipasslem1  31124  ipasslem2  31125  ipasslem4  31127  ipasslem5  31128  ipasslem8  31130  ipblnfi  31148  ip2eqi  31149  ubthlem1  31163  htthlem  31210  h2hmetdval  31271  axhvcom-zf  31276  axhis1-zf  31287  axhis4-zf  31290  hvm1neg  31325  hvsub4  31330  hvsubass  31337  hvsubdistr2  31343  hv2times  31354  hvsubcan  31367  hvsubcan2  31368  his2sub  31385  norm-i  31422  normpyc  31439  hhip  31470  hhph  31471  norm1exi  31543  hhssabloilem  31554  hhssnv  31557  hhshsslem2  31561  hhssmetdval  31570  shscli  31610  shunssi  31661  shsleji  31663  shsidmi  31677  spanunsni  31872  h1datomi  31874  spansncvi  31945  pjss2i  31973  pjssmii  31974  pjocini  31991  homullid  32093  honegdi  32102  ho2times  32112  nmopge0  32204  nmopgt0  32205  nmfnge0  32220  lnopaddi  32264  lnopmuli  32265  lnopsubi  32267  hmopbdoptHIL  32281  nmbdoplbi  32317  nmcoplbi  32321  nmophmi  32324  lnopconi  32327  lnfnaddi  32336  lnfnsubi  32339  nmbdfnlbi  32342  nmcfnlbi  32345  lnfnconi  32348  imaelshi  32351  cnlnadjlem2  32361  cnlnadjlem7  32366  nmoptrii  32387  nmopcoi  32388  adjcoi  32393  nmopcoadji  32394  bracnlnval  32407  leopmul  32427  opsqrlem1  32433  opsqrlem6  32438  hmopidmpji  32445  sto2i  32530  strlem1  32543  atcveq0  32641  atcv0eq  32672  atomli  32675  atcvati  32679  atcvat3i  32689  cdjreui  32725  cdj1i  32726  xdiv0  33189  xdivpnfrp  33193  mhmhmeotmd  34262  rezh  34304  qqhucn  34327  blsconn  35669  cnllysconn  35670  sate0fv0  35842  prv0  35855  sinccvglem  36097  opnrebl2  36755  ptrecube  38194  poimirlem6  38200  poimirlem7  38201  poimirlem29  38223  poimirlem30  38224  opnmbllem0  38230  mblfinlem3  38233  mblfinlem4  38234  ismblfin  38235  voliunnfl  38238  ftc1anclem5  38271  ftc1anclem7  38273  ftc1anclem8  38274  ftc1anc  38275  heiborlem7  38391  rrnequiv  38409  ismrer1  38412  el3v1  38804  preuniqval  39070  cnaddcom  39671  lcmineqlem1  42721  sn-ltaddpos  43152  mapco2  43373  mzpaddmpt  43399  mzpmulmpt  43400  zindbi  43600  mpaaeu  43804  tfsconcat0b  44000  eel000cT  45338  eel0TT  45339  supminfxr  46105  fmtno4prmfac  48248  pgn4cyclex  48815  aacllem  50510