Theorem mp3an1 1449

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  1452  mp3an1i  1455  mp3anl1  1456  mp3an  1462  mp3an2i  1467  mp3an3an  1468  onint  7792  wfrlem12OLD  8342  tfrlem9  8407  oaord1  8571  oaword2  8573  oawordeulem  8574  oa00  8579  omword1  8593  omword2  8594  omlimcl  8598  oeoelem  8618  nnaordex  8658  naddword1  8711  undom  9081  rexdif1enOLD  9181  sucdom2  9225  enp1iOLD  9296  fodomfi  9332  fodomfib  9351  dffi3  9453  unbnn3  9681  ttrcltr  9738  frmin  9771  frrlem16  9780  pwdjuen  10204  zorn2  10528  zornn0  10530  ttukey  10540  brdom7disj  10553  brdom6disj  10554  muladd11  11413  negsubdi  11547  mulneg1  11681  ltaddpos  11735  addge01  11755  reccl  11911  recid  11918  recid2  11919  div0  11937  recdiv2  11962  divdiv23zi  12002  ltmul12a  12105  lemul12a  12107  mulgt1OLD  12108  ltmulgt11  12109  gt0div  12116  ge0div  12117  lediv12a  12143  ledivp1  12152  ltdiv23i  12174  ledivp1i  12175  ltdivp1i  12176  infm3  12209  8th4div3  12469  gtndiv  12678  nn0ind  12696  xrre2  13194  2resupmax  13212  qsqueeze  13225  xmulpnf1  13298  xlemul1a  13312  ioorebas  13473  elfz0ubfz0  13654  le2sq2  14157  expubnd  14199  crreczi  14249  bccl  14343  hashbc  14474  wrdred1hash  14581  ccatlid  14606  shftfval  15091  sgnp  15111  sqreulem  15380  binom1p  15849  fallrisefac  16043  efsub  16118  efi4p  16155  sinadd  16182  cosadd  16183  demoivreALT  16219  rpnnen2lem4  16235  odd2np1  16360  opoe  16382  omoe  16383  opeo  16384  omeo  16385  divalglem4  16415  divalglem9  16420  gcdcllem3  16520  gcdadd  16545  algcvgblem  16596  isprm3  16702  1arith2  16948  vdwap0  16996  vdwap1  16997  ipolt  18549  smndex1sgrp  18890  f1otrspeq  19433  rmodislmod  20896  cnfldneg  21370  cnflddiv  21375  cnflddivOLD  21376  cnfldmulg  21378  cnfldexp  21379  zringsub  21428  zringmulg  21429  zringsubgval  21443  remulg  21579  resubgval  21581  thlleval  21672  mplsubrglem  21978  evls1rhm  22274  iccordt  23168  bl2ioo  24749  xrsblre  24769  iccntr  24779  icccmplem3  24782  reconnlem2  24785  opnreen  24789  mpomulcn  24827  iccpnfcnv  24911  cnllycmp  24924  pcoptcl  24990  ismbl2  25498  cmmbl  25505  nulmbl  25506  unmbl  25508  voliunlem2  25522  ioombl1  25533  opnmbllem  25572  mbfima  25601  ellimc3  25850  limcflf  25852  coe1termlem  26233  dvnply2  26265  dvnply  26266  reeff1o  26427  sinperlem  26458  resinf1o  26514  logeftb  26561  logge0  26583  efopn  26636  loglesqrt  26740  logrec  26742  xrlimcnp  26947  ppinncl  27153  chtrpcl  27154  bposlem2  27265  bposlem8  27271  lgsdir2  27310  1lgs  27320  nosupno  27684  nosupbday  27686  noinfno  27699  noinfbday  27701  noetasuplem4  27717  lrrecfr  27912  sltmul  28098  ax5seglem2  28874  axcontlem2  28910  fusgrfis  29275  3cyclfrgrrn  30233  isgrpoi  30445  imsmetlem  30637  nmcvcn  30642  ipval2  30654  lnocoi  30704  nmlno0lem  30740  nmblolbii  30746  blometi  30750  blocnilem  30751  blocni  30752  ipasslem1  30778  ipasslem2  30779  ipasslem4  30781  ipasslem5  30782  ipasslem8  30784  ipblnfi  30802  ip2eqi  30803  ubthlem1  30817  htthlem  30864  h2hmetdval  30925  axhvcom-zf  30930  axhis1-zf  30941  axhis4-zf  30944  hvm1neg  30979  hvsub4  30984  hvsubass  30991  hvsubdistr2  30997  hv2times  31008  hvsubcan  31021  hvsubcan2  31022  his2sub  31039  norm-i  31076  normpyc  31093  hhip  31124  hhph  31125  norm1exi  31197  hhssabloilem  31208  hhssnv  31211  hhshsslem2  31215  hhssmetdval  31224  shscli  31264  shunssi  31315  shsleji  31317  shsidmi  31331  spanunsni  31526  h1datomi  31528  spansncvi  31599  pjss2i  31627  pjssmii  31628  pjocini  31645  homullid  31747  honegdi  31756  ho2times  31766  nmopge0  31858  nmopgt0  31859  nmfnge0  31874  lnopaddi  31918  lnopmuli  31919  lnopsubi  31921  hmopbdoptHIL  31935  nmbdoplbi  31971  nmcoplbi  31975  nmophmi  31978  lnopconi  31981  lnfnaddi  31990  lnfnsubi  31993  nmbdfnlbi  31996  nmcfnlbi  31999  lnfnconi  32002  imaelshi  32005  cnlnadjlem2  32015  cnlnadjlem7  32020  nmoptrii  32041  nmopcoi  32042  adjcoi  32047  nmopcoadji  32048  bracnlnval  32061  leopmul  32081  opsqrlem1  32087  opsqrlem6  32092  hmopidmpji  32099  sto2i  32184  strlem1  32197  atcveq0  32295  atcv0eq  32326  atomli  32329  atcvati  32333  atcvat3i  32343  cdjreui  32379  cdj1i  32380  xdiv0  32851  xdivpnfrp  32855  mhmhmeotmd  33885  rezh  33929  qqhucn  33952  blsconn  35208  cnllysconn  35209  sate0fv0  35381  prv0  35394  sinccvglem  35636  opnrebl2  36281  ptrecube  37586  poimirlem6  37592  poimirlem7  37593  poimirlem29  37615  poimirlem30  37616  opnmbllem0  37622  mblfinlem3  37625  mblfinlem4  37626  ismblfin  37627  voliunnfl  37630  ftc1anclem5  37663  ftc1anclem7  37665  ftc1anclem8  37666  ftc1anc  37667  heiborlem7  37783  rrnequiv  37801  ismrer1  37804  el3v1  38184  cnaddcom  38932  lcmineqlem1  41989  2xp3dxp2ge1d  42201  sn-ltaddpos  42434  mapco2  42689  mzpaddmpt  42715  mzpmulmpt  42716  zindbi  42921  mpaaeu  43125  tfsconcat0b  43321  eel000cT  44680  eel0TT  44681  supminfxr  45432  fmtno4prmfac  47517  aacllem  49328