MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an1 Structured version   Visualization version   GIF version

Theorem mp3an1 1560
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
StepHypRef Expression
1 mp3an1.1 . 2 𝜑
2 mp3an1.2 . . 3 ((𝜑𝜓𝜒) → 𝜃)
323expb 1114 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 708 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072
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 197  df-an 385  df-3an 1074
This theorem is referenced by:  mp3an12  1563  mp3an1i  1566  mp3anl1  1567  mp3an  1573  mp3an2i  1578  mp3an3an  1579  onint  7161  wfrlem12  7596  wfrlem17  7601  tfrlem9  7651  oaord1  7802  oaword2  7804  oawordeulem  7805  oa00  7810  omword1  7824  omword2  7825  omlimcl  7829  oeoelem  7849  nnaordex  7889  enp1i  8362  unfilem2  8392  dffi3  8504  unbnn3  8731  pwcdaen  9219  ackbij1b  9273  zorn2  9540  zornn0  9542  ttukey  9552  brdom7disj  9565  brdom6disj  9566  wunex2  9772  muladd11  10418  00id  10423  mul02  10426  negsubdi  10549  mulneg1  10678  ltaddpos  10730  addge01  10750  reccl  10904  recid  10911  recid2  10912  recdiv2  10950  divdiv23zi  10990  ltmul12a  11091  lemul12a  11093  mulgt1  11094  ltmulgt11  11095  gt0div  11101  ge0div  11102  lediv12a  11128  ledivp1  11137  ltdiv23i  11160  ledivp1i  11161  ltdivp1i  11162  infm3  11194  nngt1ne1  11259  8th4div3  11464  gtndiv  11666  nn0ind  11684  fnn0ind  11688  supminf  11988  xrre2  12214  2resupmax  12232  qsqueeze  12245  xmulpnf1  12317  xlemul1a  12331  xrub  12355  ioorebas  12488  elfz0ubfz0  12657  expubnd  13135  le2sq2  13153  crreczi  13203  bernneq  13204  faclbnd5  13299  faclbnd6  13300  bccl  13323  hashbc  13449  wrdred1hash  13557  ccatlid  13578  shftfval  14029  sgnp  14049  mulre  14080  sqrlem4  14205  sqrlem7  14208  sqreulem  14318  binom1p  14782  0.999...OLD  14832  fallrisefac  14975  bpoly3  15008  efsub  15049  efi4p  15086  sinadd  15113  cosadd  15114  cos2t  15127  cos2tsin  15128  sin01gt0  15139  cos01gt0  15140  absefib  15147  efieq1re  15148  demoivreALT  15150  rpnnen2lem4  15165  odd2np1  15287  opoe  15309  omoe  15310  opeo  15311  omeo  15312  divalglem0  15338  divalglem4  15341  divalglem9  15346  gcdcllem3  15445  gcdn0gt0  15461  gcdadd  15469  gcdmultiple  15491  algcvgblem  15512  algcvga  15514  isprm3  15618  coprm  15645  pythagtriplem4  15746  pythagtriplem11  15752  pythagtriplem12  15753  pythagtriplem13  15754  pythagtriplem14  15755  infpn2  15839  1arith2  15854  vdwap0  15902  vdwap1  15903  ipolt  17380  gsumval2a  17500  f1otrspeq  18087  rmodislmod  19153  mplsubrglem  19661  evls1rhm  19909  cnfldneg  19994  cnflddiv  19998  cnfldmulg  20000  cnfldexp  20001  zringmulg  20048  remulg  20175  resubgval  20177  thlleval  20264  frlmsslsp  20357  neiptoptop  21157  iccordt  21240  qustgplem  22145  bl2ioo  22816  ioo2blex  22818  blssioo  22819  tgioo  22820  xrsblre  22835  iccntr  22845  icccmplem3  22848  reconnlem2  22851  opnreen  22855  iccpnfcnv  22964  cnllycmp  22976  pcoptcl  23041  ovolmge0  23465  ovolctb2  23480  ismbl2  23515  cmmbl  23522  nulmbl  23523  unmbl  23525  voliunlem1  23538  voliunlem2  23539  ioombl1  23550  opnmbllem  23589  mbfima  23618  i1fsub  23694  itg1sub  23695  ellimc3  23862  limcflf  23864  dvcnvre  24001  coe1termlem  24233  dgrsub  24247  dvnply2  24261  dvnply  24262  reeff1o  24420  sinperlem  24452  sincosq1eq  24484  resinf1o  24502  logeftb  24550  logge0  24571  logdivlti  24586  efopn  24624  logtayl2  24628  loglesqrt  24719  logrec  24721  xrlimcnp  24915  ppinncl  25120  chtrpcl  25121  bposlem2  25230  bposlem8  25236  lgsdir2  25275  1lgs  25285  brbtwn2  26005  colinearalglem4  26009  ax5seglem1  26028  ax5seglem2  26029  axcontlem2  26065  axcontlem4  26067  axcontlem7  26070  fusgrfis  26442  3cyclfrgrrn  27461  isgrpoi  27682  imsmetlem  27875  nmcvcn  27880  ipval2  27892  lnocoi  27942  nmlno0lem  27978  nmblolbii  27984  blometi  27988  blocnilem  27989  blocni  27990  ipasslem1  28016  ipasslem2  28017  ipasslem4  28019  ipasslem5  28020  ipasslem8  28022  ipblnfi  28041  ip2eqi  28042  ubthlem1  28056  htthlem  28104  h2hmetdval  28165  axhvcom-zf  28170  axhis1-zf  28181  axhis4-zf  28184  hvm1neg  28219  hvsub4  28224  hvsubass  28231  hvsubdistr2  28237  hv2times  28248  hvsubcan  28261  hvsubcan2  28262  his2sub  28279  norm-i  28316  normpyc  28333  hhip  28364  hhph  28365  norm1exi  28437  hhssabloilem  28448  hhssnv  28451  hhshsslem2  28455  hhssmetdval  28465  shscli  28506  shunssi  28557  shsleji  28559  shsidmi  28573  spanunsni  28768  h1datomi  28770  spansncvi  28841  pjss2i  28869  pjssmii  28870  pjocini  28887  homulid2  28989  honegdi  28998  ho2times  29008  nmopge0  29100  nmopgt0  29101  nmfnge0  29116  lnopaddi  29160  lnopmuli  29161  lnopsubi  29163  hmopbdoptHIL  29177  nmbdoplbi  29213  nmcoplbi  29217  nmophmi  29220  lnopconi  29223  lnfnaddi  29232  lnfnsubi  29235  nmbdfnlbi  29238  nmcfnlbi  29241  lnfnconi  29244  imaelshi  29247  cnlnadjlem2  29257  cnlnadjlem7  29262  nmoptrii  29283  nmopcoi  29284  adjcoi  29289  nmopcoadji  29290  bracnlnval  29303  leopmul  29323  opsqrlem1  29329  opsqrlem6  29334  hmopidmpji  29341  sto2i  29426  strlem1  29439  atcveq0  29537  atcv0eq  29568  atomli  29571  atcvati  29575  atcvat3i  29585  cdjreui  29621  cdj1i  29622  xdiv0  29967  xdivpnfrp  29971  mhmhmeotmd  30303  rezh  30345  qqhucn  30366  blsconn  31554  cnllysconn  31555  sinccvglem  31894  nosupno  32176  nosupbday  32178  noetalem3  32192  opnrebl2  32643  ptrecube  33740  poimirlem6  33746  poimirlem7  33747  poimirlem29  33769  poimirlem30  33770  opnmbllem0  33776  mblfinlem3  33779  mblfinlem4  33780  ismblfin  33781  voliunnfl  33784  ftc1anclem5  33820  ftc1anclem7  33822  ftc1anclem8  33823  ftc1anc  33824  heiborlem7  33947  rrnequiv  33965  ismrer1  33968  el3v1  34332  cnaddcom  34780  mapco2  37798  mzpaddmpt  37824  mzpmulmpt  37825  zindbi  38031  mpaaeu  38240  eel000cT  39448  eel0TT  39449  supminfxr  40210  fmtno4prmfac  42012  zringsubgval  42711  aacllem  43078
  Copyright terms: Public domain W3C validator