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

Theorem bitr3id 288
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
bitr3id.1 (𝜓𝜑)
bitr3id.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
bitr3id (𝜒 → (𝜑𝜃))

Proof of Theorem bitr3id
StepHypRef Expression
1 bitr3id.1 . . 3 (𝜓𝜑)
21bicomi 227 . 2 (𝜑𝜓)
3 bitr3id.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 286 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209
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 210
This theorem is referenced by:  3bitr3g  316  biass  389  sbcom2  2168  19.16  2228  19.19  2232  sbbibOLD  2290  sbal2OLD  2574  necon1bbid  3050  rspc2gv  3607  elabgt  3636  reuxfr1d  3716  sbceq1a  3758  sbcralt  3828  sbccsb2  4358  csbie2df  4364  reuprg0  4612  disjxun  5040  dmopab2rex  5763  dfres3  5836  xp11  6010  ressn  6114  fnssresb  6449  dmfco  6739  dffo4  6851  f1ompt  6857  funressn  6903  elunirnALT  6994  fliftf  7052  resoprab2  7255  elrnmpores  7272  ralrnmpo  7273  iunpw  7478  ordunisuc2  7544  tfis  7554  tfinds  7559  dfom2  7567  fiun  7630  f1iun  7631  opiota  7743  1stconst  7782  2ndconst  7783  fnsuppeq0  7845  iinon  7964  dfsmo2  7971  oeeui  8215  omabs  8261  brecop  8377  ixpsnf1o  8489  boxcutc  8492  ac6sfi  8750  wemapwe  9148  sdom2en01  9713  ac6num  9890  zorn2lem7  9913  ttukeylem6  9925  alephval2  9983  fpwwe2  10054  fpwwe  10057  nqereu  10340  suplem2pr  10464  map2psrpr  10521  supsrlem  10522  fimaxre3  11575  infm3  11587  crne0  11618  nn1suc  11647  xmulneg1  12650  supxrbnd1  12702  supxrbnd2  12703  iccneg  12850  wrdmap  13889  wrdind  14075  rtrclreclem3  14410  cnpart  14590  sqrt00  14614  lo1resb  14912  o1resb  14914  absefib  15542  efieq1re  15543  sadadd2lem2  15788  saddisjlem  15802  prmind2  16018  isprm7  16041  mreacs  16920  issubc  17096  isfunc  17125  pospo  17574  mndind  17983  eqgval  18320  resscntz  18453  frgpuplem  18889  qusabl  18976  dmdprd  19111  dprdcntz2  19151  dprd2d2  19157  isnzr2  20027  chrdvds  20218  chrcong  20219  znleval  20244  isphld  20341  mpfind  20777  gsummoncoe1  20931  pf1ind  20977  smadiadetr  21278  mp2pm2mplem4  21412  isclo  21690  ist1-2  21950  isnrm2  21961  bwth  22013  nconnsubb  22026  subislly  22084  ptclsg  22218  qtopcld  22316  kqcldsat  22336  qustgplem  22724  tsmssubm  22746  ustuqtop  22850  utop2nei  22854  blval2  23167  caucfil  23885  ioorinv  24178  mbfss  24248  iblss2  24407  dvivthlem1  24609  lhop1  24615  deg1leb  24694  reeff1o  25040  sincosq3sgn  25091  sincosq4sgn  25092  dcubic  25430  efrlim  25553  fsumharmonic  25595  isppw  25697  issqf  25719  fsumdvdsmul  25778  ppiub  25786  lgsdinn0  25927  tglngne  26342  tgelrnln  26422  axlowdimlem14  26747  nbgrssovtx  27149  clwwlknclwwlkdif  27762  eupth2lem2  28002  fusgr2wsp2nb  28117  h2hlm  28761  isch2  29004  ch0pss  29226  nmcfnlbi  29833  jplem1  30049  hatomistici  30143  mdsymlem5  30188  cdjreui  30213  dfimafnf  30389  funcnvmpt  30420  fpwrelmap  30479  nn0min  30546  wrdt2ind  30637  swrdrn3  30639  isarchi  30842  zarcls  31196  ordtconnlem1  31241  esumfsup  31403  esumpcvgval  31411  measvuni  31547  aean  31577  eulerpartlemgh  31710  ballotlemsima  31847  sgn3da  31873  bnj1468  32192  subfacp1lem2a  32501  subfacp1lem6  32506  goeleq12bg  32670  dmopab3rexdif  32726  eldm3  33071  onsuct0  33863  currysetlem1  34343  bj-restsn  34458  ptrest  35014  ptrecube  35015  poimirlem2  35017  poimirlem23  35038  sdclem2  35138  fdc  35141  fdc1  35142  istotbnd3  35167  sstotbnd  35171  prdstotbnd  35190  rrncmslem  35228  brinxprnres  35666  brcnvrabga  35717  alrmomodm  35731  br1cossxrnres  35806  lub0N  36443  glb0N  36447  cdlemefrs29bpre0  37650  dvhb1dimN  38240  dvhopellsm  38371  dibord  38413  dochnel2  38646  mapdvalc  38883  mapdval4N  38886  diophin  39643  diophun  39644  diophrex  39646  3rexfrabdioph  39668  6rexfrabdioph  39670  7rexfrabdioph  39671  zindbi  39817  rababg  40203  relexpnul  40309  clsk1independent  40682  scottabf  40882  hashnzfzclim  40960  fveqsb  41091  infxrbnd2  41940  cncfiooicclem1  42474  stoweidlem35  42616  tz6.12-afv  43668  ndmaovg  43679  tz6.12-afv2  43735  ich2exprop  43927  prprspr2  43974  line2x  45107  line2y  45108  itsclc0b  45125  aacllem  45268
  Copyright terms: Public domain W3C validator