Theorem mp3an1 1450

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

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

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 1088

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7782  wfrlem12OLD  8332  tfrlem9  8397  oaord1  8561  oaword2  8563  oawordeulem  8564  oa00  8569  omword1  8583  omword2  8584  omlimcl  8588  oeoelem  8608  nnaordex  8648  naddword1  8701  undom  9071  rexdif1enOLD  9171  sucdom2  9215  enp1iOLD  9284  fodomfi  9320  fodomfib  9339  dffi3  9441  unbnn3  9671  ttrcltr  9728  frmin  9761  frrlem16  9770  pwdjuen  10194  zorn2  10518  zornn0  10520  ttukey  10530  brdom7disj  10543  brdom6disj  10544  muladd11  11403  negsubdi  11537  mulneg1  11671  ltaddpos  11725  addge01  11745  reccl  11901  recid  11908  recid2  11909  div0  11927  recdiv2  11952  divdiv23zi  11992  ltmul12a  12095  lemul12a  12097  mulgt1OLD  12098  ltmulgt11  12099  gt0div  12106  ge0div  12107  lediv12a  12133  ledivp1  12142  ltdiv23i  12164  ledivp1i  12165  ltdivp1i  12166  infm3  12199  8th4div3  12459  gtndiv  12668  nn0ind  12686  xrre2  13184  2resupmax  13202  qsqueeze  13215  xmulpnf1  13288  xlemul1a  13302  ioorebas  13466  elfz0ubfz0  13647  le2sq2  14151  expubnd  14194  crreczi  14244  bccl  14338  hashbc  14469  wrdred1hash  14577  ccatlid  14602  shftfval  15087  sgnp  15107  sqreulem  15376  binom1p  15845  fallrisefac  16039  efsub  16116  efi4p  16153  sinadd  16180  cosadd  16181  demoivreALT  16217  rpnnen2lem4  16233  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  divalglem4  16413  divalglem9  16418  gcdcllem3  16518  gcdadd  16543  algcvgblem  16594  isprm3  16700  1arith2  16946  vdwap0  16994  vdwap1  16995  ipolt  18543  smndex1sgrp  18884  f1otrspeq  19426  rmodislmod  20885  cnfldneg  21356  cnflddiv  21361  cnflddivOLD  21362  cnfldmulg  21364  cnfldexp  21365  zringsub  21414  zringmulg  21415  zringsubgval  21429  remulg  21565  resubgval  21567  thlleval  21656  mplsubrglem  21962  evls1rhm  22258  iccordt  23150  bl2ioo  24729  xrsblre  24749  iccntr  24759  icccmplem3  24762  reconnlem2  24765  opnreen  24769  mpomulcn  24807  iccpnfcnv  24891  cnllycmp  24904  pcoptcl  24970  ismbl2  25478  cmmbl  25485  nulmbl  25486  unmbl  25488  voliunlem2  25502  ioombl1  25513  opnmbllem  25552  mbfima  25581  ellimc3  25830  limcflf  25832  coe1termlem  26213  dvnply2  26245  dvnply  26246  reeff1o  26407  sinperlem  26439  resinf1o  26495  logeftb  26542  logge0  26564  efopn  26617  loglesqrt  26721  logrec  26723  xrlimcnp  26928  ppinncl  27134  chtrpcl  27135  bposlem2  27246  bposlem8  27252  lgsdir2  27291  1lgs  27301  nosupno  27665  nosupbday  27667  noinfno  27680  noinfbday  27682  noetasuplem4  27698  lrrecfr  27893  sltmul  28079  ax5seglem2  28854  axcontlem2  28890  fusgrfis  29255  3cyclfrgrrn  30213  isgrpoi  30425  imsmetlem  30617  nmcvcn  30622  ipval2  30634  lnocoi  30684  nmlno0lem  30720  nmblolbii  30726  blometi  30730  blocnilem  30731  blocni  30732  ipasslem1  30758  ipasslem2  30759  ipasslem4  30761  ipasslem5  30762  ipasslem8  30764  ipblnfi  30782  ip2eqi  30783  ubthlem1  30797  htthlem  30844  h2hmetdval  30905  axhvcom-zf  30910  axhis1-zf  30921  axhis4-zf  30924  hvm1neg  30959  hvsub4  30964  hvsubass  30971  hvsubdistr2  30977  hv2times  30988  hvsubcan  31001  hvsubcan2  31002  his2sub  31019  norm-i  31056  normpyc  31073  hhip  31104  hhph  31105  norm1exi  31177  hhssabloilem  31188  hhssnv  31191  hhshsslem2  31195  hhssmetdval  31204  shscli  31244  shunssi  31295  shsleji  31297  shsidmi  31311  spanunsni  31506  h1datomi  31508  spansncvi  31579  pjss2i  31607  pjssmii  31608  pjocini  31625  homullid  31727  honegdi  31736  ho2times  31746  nmopge0  31838  nmopgt0  31839  nmfnge0  31854  lnopaddi  31898  lnopmuli  31899  lnopsubi  31901  hmopbdoptHIL  31915  nmbdoplbi  31951  nmcoplbi  31955  nmophmi  31958  lnopconi  31961  lnfnaddi  31970  lnfnsubi  31973  nmbdfnlbi  31976  nmcfnlbi  31979  lnfnconi  31982  imaelshi  31985  cnlnadjlem2  31995  cnlnadjlem7  32000  nmoptrii  32021  nmopcoi  32022  adjcoi  32027  nmopcoadji  32028  bracnlnval  32041  leopmul  32061  opsqrlem1  32067  opsqrlem6  32072  hmopidmpji  32079  sto2i  32164  strlem1  32177  atcveq0  32275  atcv0eq  32306  atomli  32309  atcvati  32313  atcvat3i  32323  cdjreui  32359  cdj1i  32360  xdiv0  32849  xdivpnfrp  32853  mhmhmeotmd  33904  rezh  33946  qqhucn  33969  blsconn  35212  cnllysconn  35213  sate0fv0  35385  prv0  35398  sinccvglem  35640  opnrebl2  36285  ptrecube  37590  poimirlem6  37596  poimirlem7  37597  poimirlem29  37619  poimirlem30  37620  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  voliunnfl  37634  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  heiborlem7  37787  rrnequiv  37805  ismrer1  37808  el3v1  38188  cnaddcom  38936  lcmineqlem1  41988  2xp3dxp2ge1d  42200  sn-ltaddpos  42431  mapco2  42685  mzpaddmpt  42711  mzpmulmpt  42712  zindbi  42917  mpaaeu  43121  tfsconcat0b  43317  eel000cT  44675  eel0TT  44676  supminfxr  45439  fmtno4prmfac  47534  aacllem  49613