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

Theorem mp3an1 1565
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 1142 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
41, 3mpan 673 1 ((𝜓𝜒) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1100
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 198  df-an 385  df-3an 1102
This theorem is referenced by:  mp3an12  1568  mp3an1i  1571  mp3anl1  1572  mp3an  1578  mp3an2i  1583  mp3an3an  1584  onint  7219  wfrlem12  7656  wfrlem17  7661  tfrlem9  7711  oaord1  7862  oaword2  7864  oawordeulem  7865  oa00  7870  omword1  7884  omword2  7885  omlimcl  7889  oeoelem  7909  nnaordex  7949  enp1i  8428  unfilem2  8458  dffi3  8570  unbnn3  8797  pwcdaen  9286  ackbij1b  9340  zorn2  9607  zornn0  9609  ttukey  9619  brdom7disj  9632  brdom6disj  9633  wunex2  9839  muladd11  10485  00id  10490  mul02  10493  negsubdi  10616  mulneg1  10745  ltaddpos  10797  addge01  10817  reccl  10971  recid  10978  recid2  10979  recdiv2  11017  divdiv23zi  11057  ltmul12a  11158  lemul12a  11160  mulgt1  11161  ltmulgt11  11162  gt0div  11168  ge0div  11169  lediv12a  11195  ledivp1  11204  ltdiv23i  11227  ledivp1i  11228  ltdivp1i  11229  infm3  11261  nngt1ne1  11327  8th4div3  11513  gtndiv  11714  nn0ind  11732  fnn0ind  11736  supminf  11988  xrre2  12213  2resupmax  12231  qsqueeze  12244  xmulpnf1  12316  xlemul1a  12330  xrub  12354  ioorebas  12488  elfz0ubfz0  12661  expubnd  13138  le2sq2  13156  crreczi  13206  bernneq  13207  faclbnd5  13299  faclbnd6  13300  bccl  13323  hashbc  13448  wrdred1hash  13556  ccatlid  13577  shftfval  14027  sgnp  14047  mulre  14078  sqrlem4  14203  sqreulem  14316  binom1p  14779  fallrisefac  14970  bpoly3  15003  efsub  15044  efi4p  15081  sinadd  15108  cosadd  15109  cos2t  15122  cos2tsin  15123  sin01gt0  15134  cos01gt0  15135  absefib  15142  efieq1re  15143  demoivreALT  15145  rpnnen2lem4  15160  odd2np1  15279  opoe  15301  omoe  15302  opeo  15303  omeo  15304  divalglem0  15330  divalglem4  15333  divalglem9  15338  gcdcllem3  15436  gcdn0gt0  15452  gcdadd  15460  gcdmultiple  15482  algcvgblem  15503  algcvga  15505  isprm3  15608  coprm  15634  pythagtriplem4  15735  pythagtriplem11  15741  pythagtriplem12  15742  pythagtriplem13  15743  pythagtriplem14  15744  infpn2  15828  1arith2  15843  vdwap0  15891  vdwap1  15892  ipolt  17358  gsumval2a  17478  f1otrspeq  18062  rmodislmod  19129  mplsubrglem  19642  evls1rhm  19889  cnfldneg  19974  cnflddiv  19978  cnfldmulg  19980  cnfldexp  19981  zringmulg  20028  remulg  20156  resubgval  20158  thlleval  20246  frlmsslsp  20339  neiptoptop  21143  iccordt  21226  qustgplem  22131  bl2ioo  22802  ioo2blex  22804  blssioo  22805  tgioo  22806  xrsblre  22821  iccntr  22831  icccmplem3  22834  reconnlem2  22837  opnreen  22841  iccpnfcnv  22950  cnllycmp  22962  pcoptcl  23027  ovolmge0  23452  ovolctb2  23467  ismbl2  23502  cmmbl  23509  nulmbl  23510  unmbl  23512  voliunlem1  23525  voliunlem2  23526  ioombl1  23537  opnmbllem  23576  mbfima  23605  i1fsub  23683  itg1sub  23684  ellimc3  23851  limcflf  23853  dvcnvre  23990  coe1termlem  24222  dgrsub  24236  dvnply2  24250  dvnply  24251  reeff1o  24409  sinperlem  24441  sincosq1eq  24473  resinf1o  24491  logeftb  24538  logge0  24559  logdivlti  24574  efopn  24612  logtayl2  24616  loglesqrt  24707  logrec  24709  xrlimcnp  24903  ppinncl  25108  chtrpcl  25109  bposlem2  25218  bposlem8  25224  lgsdir2  25263  1lgs  25273  brbtwn2  25993  colinearalglem4  25997  ax5seglem1  26016  ax5seglem2  26017  axcontlem2  26053  axcontlem4  26055  axcontlem7  26058  fusgrfis  26432  3cyclfrgrrn  27455  isgrpoi  27675  imsmetlem  27867  nmcvcn  27872  ipval2  27884  lnocoi  27934  nmlno0lem  27970  nmblolbii  27976  blometi  27980  blocnilem  27981  blocni  27982  ipasslem1  28008  ipasslem2  28009  ipasslem4  28011  ipasslem5  28012  ipasslem8  28014  ipblnfi  28033  ip2eqi  28034  ubthlem1  28048  htthlem  28096  h2hmetdval  28157  axhvcom-zf  28162  axhis1-zf  28173  axhis4-zf  28176  hvm1neg  28211  hvsub4  28216  hvsubass  28223  hvsubdistr2  28229  hv2times  28240  hvsubcan  28253  hvsubcan2  28254  his2sub  28271  norm-i  28308  normpyc  28325  hhip  28356  hhph  28357  norm1exi  28429  hhssabloilem  28440  hhssnv  28443  hhshsslem2  28447  hhssmetdval  28457  shscli  28498  shunssi  28549  shsleji  28551  shsidmi  28565  spanunsni  28760  h1datomi  28762  spansncvi  28833  pjss2i  28861  pjssmii  28862  pjocini  28879  homulid2  28981  honegdi  28990  ho2times  29000  nmopge0  29092  nmopgt0  29093  nmfnge0  29108  lnopaddi  29152  lnopmuli  29153  lnopsubi  29155  hmopbdoptHIL  29169  nmbdoplbi  29205  nmcoplbi  29209  nmophmi  29212  lnopconi  29215  lnfnaddi  29224  lnfnsubi  29227  nmbdfnlbi  29230  nmcfnlbi  29233  lnfnconi  29236  imaelshi  29239  cnlnadjlem2  29249  cnlnadjlem7  29254  nmoptrii  29275  nmopcoi  29276  adjcoi  29281  nmopcoadji  29282  bracnlnval  29295  leopmul  29315  opsqrlem1  29321  opsqrlem6  29326  hmopidmpji  29333  sto2i  29418  strlem1  29431  atcveq0  29529  atcv0eq  29560  atomli  29563  atcvati  29567  atcvat3i  29577  cdjreui  29613  cdj1i  29614  xdiv0  29956  xdivpnfrp  29960  mhmhmeotmd  30292  rezh  30334  qqhucn  30355  blsconn  31543  cnllysconn  31544  sinccvglem  31882  nosupno  32164  nosupbday  32166  noetalem3  32180  opnrebl2  32631  ptrecube  33716  poimirlem6  33722  poimirlem7  33723  poimirlem29  33745  poimirlem30  33746  opnmbllem0  33752  mblfinlem3  33755  mblfinlem4  33756  ismblfin  33757  voliunnfl  33760  ftc1anclem5  33795  ftc1anclem7  33797  ftc1anclem8  33798  ftc1anc  33799  heiborlem7  33921  rrnequiv  33939  ismrer1  33942  el3v1  34303  cnaddcom  34746  mapco2  37774  mzpaddmpt  37800  mzpmulmpt  37801  zindbi  38006  mpaaeu  38215  eel000cT  39420  eel0TT  39421  supminfxr  40167  fmtno4prmfac  42053  zringsubgval  42745  aacllem  43112
  Copyright terms: Public domain W3C validator