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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 690	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  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7810  wfrlem12OLD  8360  tfrlem9  8425  oaord1  8589  oaword2  8591  oawordeulem  8592  oa00  8597  omword1  8611  omword2  8612  omlimcl  8616  oeoelem  8636  nnaordex  8676  naddword1  8729  undom  9099  rexdif1enOLD  9199  sucdom2  9243  enp1iOLD  9314  fodomfi  9350  fodomfib  9369  dffi3  9471  unbnn3  9699  ttrcltr  9756  frmin  9789  frrlem16  9798  pwdjuen  10222  zorn2  10546  zornn0  10548  ttukey  10558  brdom7disj  10571  brdom6disj  10572  muladd11  11431  negsubdi  11565  mulneg1  11699  ltaddpos  11753  addge01  11773  reccl  11929  recid  11936  recid2  11937  div0  11955  recdiv2  11980  divdiv23zi  12020  ltmul12a  12123  lemul12a  12125  mulgt1OLD  12126  ltmulgt11  12127  gt0div  12134  ge0div  12135  lediv12a  12161  ledivp1  12170  ltdiv23i  12192  ledivp1i  12193  ltdivp1i  12194  infm3  12227  8th4div3  12486  gtndiv  12695  nn0ind  12713  xrre2  13212  2resupmax  13230  qsqueeze  13243  xmulpnf1  13316  xlemul1a  13330  ioorebas  13491  elfz0ubfz0  13672  le2sq2  14175  expubnd  14217  crreczi  14267  bccl  14361  hashbc  14492  wrdred1hash  14599  ccatlid  14624  shftfval  15109  sgnp  15129  sqreulem  15398  binom1p  15867  fallrisefac  16061  efsub  16136  efi4p  16173  sinadd  16200  cosadd  16201  demoivreALT  16237  rpnnen2lem4  16253  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  divalglem4  16433  divalglem9  16438  gcdcllem3  16538  gcdadd  16563  algcvgblem  16614  isprm3  16720  1arith2  16966  vdwap0  17014  vdwap1  17015  ipolt  18580  smndex1sgrp  18921  f1otrspeq  19465  rmodislmod  20928  cnfldneg  21408  cnflddiv  21413  cnflddivOLD  21414  cnfldmulg  21416  cnfldexp  21417  zringsub  21466  zringmulg  21467  zringsubgval  21481  remulg  21625  resubgval  21627  thlleval  21718  mplsubrglem  22024  evls1rhm  22326  iccordt  23222  bl2ioo  24813  xrsblre  24833  iccntr  24843  icccmplem3  24846  reconnlem2  24849  opnreen  24853  mpomulcn  24891  iccpnfcnv  24975  cnllycmp  24988  pcoptcl  25054  ismbl2  25562  cmmbl  25569  nulmbl  25570  unmbl  25572  voliunlem2  25586  ioombl1  25597  opnmbllem  25636  mbfima  25665  ellimc3  25914  limcflf  25916  coe1termlem  26297  dvnply2  26329  dvnply  26330  reeff1o  26491  sinperlem  26522  resinf1o  26578  logeftb  26625  logge0  26647  efopn  26700  loglesqrt  26804  logrec  26806  xrlimcnp  27011  ppinncl  27217  chtrpcl  27218  bposlem2  27329  bposlem8  27335  lgsdir2  27374  1lgs  27384  nosupno  27748  nosupbday  27750  noinfno  27763  noinfbday  27765  noetasuplem4  27781  lrrecfr  27976  sltmul  28162  ax5seglem2  28944  axcontlem2  28980  fusgrfis  29347  3cyclfrgrrn  30305  isgrpoi  30517  imsmetlem  30709  nmcvcn  30714  ipval2  30726  lnocoi  30776  nmlno0lem  30812  nmblolbii  30818  blometi  30822  blocnilem  30823  blocni  30824  ipasslem1  30850  ipasslem2  30851  ipasslem4  30853  ipasslem5  30854  ipasslem8  30856  ipblnfi  30874  ip2eqi  30875  ubthlem1  30889  htthlem  30936  h2hmetdval  30997  axhvcom-zf  31002  axhis1-zf  31013  axhis4-zf  31016  hvm1neg  31051  hvsub4  31056  hvsubass  31063  hvsubdistr2  31069  hv2times  31080  hvsubcan  31093  hvsubcan2  31094  his2sub  31111  norm-i  31148  normpyc  31165  hhip  31196  hhph  31197  norm1exi  31269  hhssabloilem  31280  hhssnv  31283  hhshsslem2  31287  hhssmetdval  31296  shscli  31336  shunssi  31387  shsleji  31389  shsidmi  31403  spanunsni  31598  h1datomi  31600  spansncvi  31671  pjss2i  31699  pjssmii  31700  pjocini  31717  homullid  31819  honegdi  31828  ho2times  31838  nmopge0  31930  nmopgt0  31931  nmfnge0  31946  lnopaddi  31990  lnopmuli  31991  lnopsubi  31993  hmopbdoptHIL  32007  nmbdoplbi  32043  nmcoplbi  32047  nmophmi  32050  lnopconi  32053  lnfnaddi  32062  lnfnsubi  32065  nmbdfnlbi  32068  nmcfnlbi  32071  lnfnconi  32074  imaelshi  32077  cnlnadjlem2  32087  cnlnadjlem7  32092  nmoptrii  32113  nmopcoi  32114  adjcoi  32119  nmopcoadji  32120  bracnlnval  32133  leopmul  32153  opsqrlem1  32159  opsqrlem6  32164  hmopidmpji  32171  sto2i  32256  strlem1  32269  atcveq0  32367  atcv0eq  32398  atomli  32401  atcvati  32405  atcvat3i  32415  cdjreui  32451  cdj1i  32452  xdiv0  32911  xdivpnfrp  32915  mhmhmeotmd  33926  rezh  33970  qqhucn  33993  blsconn  35249  cnllysconn  35250  sate0fv0  35422  prv0  35435  sinccvglem  35677  opnrebl2  36322  ptrecube  37627  poimirlem6  37633  poimirlem7  37634  poimirlem29  37656  poimirlem30  37657  opnmbllem0  37663  mblfinlem3  37666  mblfinlem4  37667  ismblfin  37668  voliunnfl  37671  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  heiborlem7  37824  rrnequiv  37842  ismrer1  37845  el3v1  38225  cnaddcom  38973  lcmineqlem1  42030  2xp3dxp2ge1d  42242  sn-ltaddpos  42471  mapco2  42726  mzpaddmpt  42752  mzpmulmpt  42753  zindbi  42958  mpaaeu  43162  tfsconcat0b  43359  eel000cT  44723  eel0TT  44724  supminfxr  45475  fmtno4prmfac  47559  aacllem  49320