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  7747  tfrlem9  8328  oaord1  8490  oaword2  8492  oawordeulem  8493  oa00  8498  omword1  8512  omword2  8513  omlimcl  8517  oeoelem  8538  nnaordex  8578  naddword1  8631  undom  9007  sucdom2  9141  fodomfi  9226  fodomfib  9243  dffi3  9348  unbnn3  9582  ttrcltr  9639  frmin  9675  frrlem16  9684  pwdjuen  10106  zorn2  10430  zornn0  10432  ttukey  10442  brdom7disj  10455  brdom6disj  10456  muladd11  11317  negsubdi  11451  mulneg1  11587  ltaddpos  11641  addge01  11661  reccl  11817  recid  11824  recid2  11825  div0  11843  recdiv2  11868  divdiv23zi  11908  ltmul12a  12011  lemul12a  12013  mulgt1OLD  12014  ltmulgt11  12015  gt0div  12022  ge0div  12023  lediv12a  12049  ledivp1  12058  ltdiv23i  12080  ledivp1i  12081  ltdivp1i  12082  infm3  12115  8th4div3  12375  gtndiv  12583  nn0ind  12601  xrre2  13099  2resupmax  13117  qsqueeze  13130  xmulpnf1  13203  xlemul1a  13217  ioorebas  13381  elfz0ubfz0  13562  le2sq2  14072  expubnd  14115  crreczi  14165  bccl  14259  hashbc  14390  wrdred1hash  14498  ccatlid  14524  shftfval  15007  sgnp  15027  sqreulem  15297  binom1p  15768  fallrisefac  15962  efsub  16039  efi4p  16076  sinadd  16103  cosadd  16104  demoivreALT  16140  rpnnen2lem4  16156  odd2np1  16282  opoe  16304  omoe  16305  opeo  16306  omeo  16307  divalglem4  16337  divalglem9  16342  gcdcllem3  16442  gcdadd  16467  algcvgblem  16518  isprm3  16624  1arith2  16870  vdwap0  16918  vdwap1  16919  ipolt  18472  smndex1sgrp  18850  f1otrspeq  19393  rmodislmod  20898  cnfldneg  21367  cnflddiv  21372  cnflddivOLD  21373  cnfldmulg  21375  cnfldexp  21376  zringsub  21427  zringmulg  21428  zringsubgval  21442  remulg  21579  resubgval  21581  thlleval  21670  mplsubrglem  21976  evls1rhm  22283  iccordt  23175  bl2ioo  24753  xrsblre  24773  iccntr  24783  icccmplem3  24786  reconnlem2  24789  opnreen  24793  mpomulcn  24831  iccpnfcnv  24915  cnllycmp  24928  pcoptcl  24994  ismbl2  25501  cmmbl  25508  nulmbl  25509  unmbl  25511  voliunlem2  25525  ioombl1  25536  opnmbllem  25575  mbfima  25604  ellimc3  25853  limcflf  25855  coe1termlem  26236  dvnply2  26268  dvnply  26269  reeff1o  26430  sinperlem  26462  resinf1o  26518  logeftb  26565  logge0  26587  efopn  26640  loglesqrt  26744  logrec  26746  xrlimcnp  26951  ppinncl  27157  chtrpcl  27158  bposlem2  27269  bposlem8  27275  lgsdir2  27314  1lgs  27324  nosupno  27688  nosupbday  27690  noinfno  27703  noinfbday  27705  noetasuplem4  27721  lrrecfr  27956  ltmuls  28149  bdayfinbndlem1  28480  ax5seglem2  29020  axcontlem2  29056  fusgrfis  29421  3cyclfrgrrn  30379  isgrpoi  30592  imsmetlem  30784  nmcvcn  30789  ipval2  30801  lnocoi  30851  nmlno0lem  30887  nmblolbii  30893  blometi  30897  blocnilem  30898  blocni  30899  ipasslem1  30925  ipasslem2  30926  ipasslem4  30928  ipasslem5  30929  ipasslem8  30931  ipblnfi  30949  ip2eqi  30950  ubthlem1  30964  htthlem  31011  h2hmetdval  31072  axhvcom-zf  31077  axhis1-zf  31088  axhis4-zf  31091  hvm1neg  31126  hvsub4  31131  hvsubass  31138  hvsubdistr2  31144  hv2times  31155  hvsubcan  31168  hvsubcan2  31169  his2sub  31186  norm-i  31223  normpyc  31240  hhip  31271  hhph  31272  norm1exi  31344  hhssabloilem  31355  hhssnv  31358  hhshsslem2  31362  hhssmetdval  31371  shscli  31411  shunssi  31462  shsleji  31464  shsidmi  31478  spanunsni  31673  h1datomi  31675  spansncvi  31746  pjss2i  31774  pjssmii  31775  pjocini  31792  homullid  31894  honegdi  31903  ho2times  31913  nmopge0  32005  nmopgt0  32006  nmfnge0  32021  lnopaddi  32065  lnopmuli  32066  lnopsubi  32068  hmopbdoptHIL  32082  nmbdoplbi  32118  nmcoplbi  32122  nmophmi  32125  lnopconi  32128  lnfnaddi  32137  lnfnsubi  32140  nmbdfnlbi  32143  nmcfnlbi  32146  lnfnconi  32149  imaelshi  32152  cnlnadjlem2  32162  cnlnadjlem7  32167  nmoptrii  32188  nmopcoi  32189  adjcoi  32194  nmopcoadji  32195  bracnlnval  32208  leopmul  32228  opsqrlem1  32234  opsqrlem6  32239  hmopidmpji  32246  sto2i  32331  strlem1  32344  atcveq0  32442  atcv0eq  32473  atomli  32476  atcvati  32480  atcvat3i  32490  cdjreui  32526  cdj1i  32527  xdiv0  33027  xdivpnfrp  33031  mhmhmeotmd  34111  rezh  34153  qqhucn  34176  blsconn  35466  cnllysconn  35467  sate0fv0  35639  prv0  35652  sinccvglem  35894  opnrebl2  36543  ptrecube  37900  poimirlem6  37906  poimirlem7  37907  poimirlem29  37929  poimirlem30  37930  opnmbllem0  37936  mblfinlem3  37939  mblfinlem4  37940  ismblfin  37941  voliunnfl  37944  ftc1anclem5  37977  ftc1anclem7  37979  ftc1anclem8  37980  ftc1anc  37981  heiborlem7  38097  rrnequiv  38115  ismrer1  38118  el3v1  38510  preuniqval  38776  cnaddcom  39377  lcmineqlem1  42428  sn-ltaddpos  42852  mapco2  43101  mzpaddmpt  43127  mzpmulmpt  43128  zindbi  43332  mpaaeu  43536  tfsconcat0b  43732  eel000cT  45087  eel0TT  45088  supminfxr  45851  fmtno4prmfac  47961  pgn4cyclex  48515  aacllem  50189