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

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

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3 (𝜓𝜑)
21bicomi 212 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 270 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194
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 195
This theorem is referenced by:  3bitr3g  300  biass  372  19.16  2087  19.19  2089  sbcom2  2337  sbal2  2353  necon1bbid  2725  elabgt  3220  sbceq1a  3317  sbcralt  3381  sbccsb2  3860  disjxun  4479  xp11  5378  ressn  5478  fnssresb  5802  dmfco  6065  dffo4  6166  f1ompt  6173  funressn  6207  elunirnALT  6290  fliftf  6341  resoprab2  6531  elrnmpt2res  6548  ralrnmpt2  6549  iunpw  6745  ordunisuc2  6811  tfis  6821  tfinds  6826  dfom2  6834  fun11iun  6893  opiota  6992  1stconst  7026  2ndconst  7027  fnsuppeq0  7084  iinon  7199  dfsmo2  7206  oeeui  7444  omabs  7489  brecop  7602  ixpsnf1o  7709  boxcutc  7712  ac6sfi  7964  wemapwe  8352  sdom2en01  8882  ac6num  9059  zorn2lem7  9082  ttukeylem6  9094  alephval2  9148  fpwwe2  9219  fpwwe  9222  nqereu  9505  suplem2pr  9629  map2psrpr  9685  supsrlem  9686  fimaxre3  10719  infm3  10734  crne0  10767  nn1suc  10795  xmulneg1  11837  supxrbnd1  11889  supxrbnd2  11890  iccneg  12032  wrdmap  13048  wrdind  13185  rtrclreclem3  13505  cnpart  13685  sqrt00  13709  lo1resb  14007  o1resb  14009  absefib  14634  efieq1re  14635  sadadd2lem2  14881  saddisjlem  14895  prmind2  15110  isprm7  15132  mreacs  16032  issubc  16208  isfunc  16237  pospo  16686  mrcmndind  17079  eqgval  17356  resscntz  17477  frgpuplem  17914  qusabl  17996  dmdprd  18125  dprdcntz2  18165  dprd2d2  18171  isnzr2  18986  mpfind  19259  gsummoncoe1  19397  pf1ind  19442  chrdvds  19599  chrcong  19600  znleval  19626  isphld  19722  smadiadetr  20201  mp2pm2mplem4  20334  isclo  20602  ist1-2  20862  isnrm2  20873  bwth  20924  nconsubb  20937  subislly  20995  ptclsg  21129  qtopcld  21227  kqcldsat  21247  qustgplem  21635  tsmssubm  21657  ustuqtop  21761  utop2nei  21765  blval2  22077  caucfil  22754  ioorinv  23026  mbfss  23095  iblss2  23254  dvivthlem1  23451  lhop1  23457  deg1leb  23535  reeff1o  23893  sincosq3sgn  23944  sincosq4sgn  23945  dcubic  24261  efrlim  24384  fsumharmonic  24426  isppw  24530  issqf  24552  fsumdvdsmul  24611  ppiub  24619  lgsdinn0  24760  tglngne  25136  tgelrnln  25216  axlowdimlem14  25526  uhgraop  25572  eupath2lem2  26244  h2hlm  27010  isch2  27253  ch0pss  27477  nmcfnlbi  28084  jplem1  28300  hatomistici  28394  mdsymlem5  28439  cdjreui  28464  reuxfr4d  28503  dfimafnf  28606  funcnvmpt  28640  fpwrelmap  28685  nn0min  28750  isarchi  28864  ordtconlem1  29095  esumfsup  29256  esumpcvgval  29264  measvuni  29401  aean  29431  eulerpartlemgh  29575  ballotlemsima  29712  ballotlemsimaOLD  29750  sgn3da  29776  bnj1468  30016  subfacp1lem2a  30262  subfacp1lem6  30267  dfres3  30745  eldm3  30748  onsuct0  31445  bj-restsn  32048  ptrest  32453  ptrecube  32454  poimirlem2  32456  poimirlem23  32477  sdclem2  32583  fdc  32586  fdc1  32587  istotbnd3  32615  sstotbnd  32619  prdstotbnd  32638  rrncmslem  32676  lub0N  33369  glb0N  33373  cdlemefrs29bpre0  34577  dvhb1dimN  35167  dvhopellsm  35299  dibord  35341  dochnel2  35574  mapdvalc  35811  mapdval4N  35814  diophin  36229  diophun  36230  diophrex  36232  3rexfrabdioph  36254  6rexfrabdioph  36256  7rexfrabdioph  36257  zindbi  36404  rababg  36780  relexpnul  36871  clsk1independent  37246  hashnzfzclim  37425  fveqsb  37560  infxrbnd2  38412  cncfiooicclem1  38666  stoweidlem35  38818  tz6.12-afv  39797  ndmaovg  39808  nbgrssovtx  40678  eupth2lem2  41479  fusgr2wsp2nb  41590  aacllem  42409
  Copyright terms: Public domain W3C validator