HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem syl5bb 531
Description: A syllogism inference from two biconditionals.
Hypotheses
Ref Expression
syl5bb.1 |- (ph -> (ps <-> ch))
syl5bb.2 |- (th <-> ps)
Assertion
Ref Expression
syl5bb |- (ph -> (th <-> ch))
Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.2 . . 3 |- (th <-> ps)
21a1i 8 . 2 |- (ph -> (th <-> ps))
3 syl5bb.1 . 2 |- (ph -> (ps <-> ch))
42, 3bitrd 527 1 |- (ph -> (th <-> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3   <-> wb 146
This theorem is referenced by:  syl5rbb 532  syl5bbr 533  3bitr4g 554  oplem1 771  19.23t 1114  sbcom 1256  necon3abid 1596  necon1abid 1615  r19.21t 1712  ceqsrexv 1885  ceqsrex2v 1886  elab2g 1896  elrabf 1900  eueq2 1914  reu8 1932  ru 1934  sbccomglem 1984  rabbirdv 2217  disjpss 2315  undif4 2321  opthpr 2481  dfiun2g 2581  elpwuni 2756  copsex4g 2789  opelopabg 2812  brabg 2813  dfid3 2831  oneqmini 3012  elsucg 3031  elsuc2g 3032  ordpwsuc 3061  dfom2 3128  opbrop 3233  opelcnvg 3291  dmsnop 3323  iss 3389  imasng 3416  cores 3491  cnvpo 3514  fncnv 3553  fununi 3555  fnssresb 3591  fnopabfv 3749  funimass4 3754  fnsnfv 3758  dmfco 3764  fvco 3765  fvopabn 3777  fvopab5 3784  elrnopabg 3791  fvimacnvi 3795  fvimacnvALT 3800  fressnfv 3829  funiunfv 3857  elunirnALT 3860  f1fv 3865  isoini 3891  f1oiso 3895  f1oweALT 3897  tfrlem1 3902  rdglim2 3940  eloprabg 3998  oprabval 4014  ndmoprgOLD 4035  2ndconst 4087  dfoprab5 4105  elrnoprabg 4114  brecop 4296  mapsn 4335  ixp0 4351  xpsnen 4421  xpdom2 4428  pw2en 4432  mapxpen 4481  abfii4 4544  fodomfib 4547  noinfep 4620  rankbnd2 4684  aceq3lem 4712  zorn2 4776  fodomb 4780  brdom7disj 4784  brdom6disj 4785  domtri 4818  cardsdomel 4832  iscard2 4834  alephnbtwn 4848  nlt1pi 5013  ltsopq 5055  genpv 5082  ltsosr 5183  suppsrlem 5201  suppsr 5202  supsrlem6 5210  suprelem 5239  supre 5240  axrrecex 5264  renegcl 5396  ltxrt 5475  ltxrltt 5480  xrlenltt 5481  ssxr 5521  divdivdivt 5749  conjmult 5761  lerec 5836  lt2msq 5837  nn1suc 5895  infm3 6009  infmsup 6023  elznn0 6104  elnn0nn 6126  zltp1let 6136  primet 6150  dfuz 6158  rebtwnz 6178  ioo0t 6313  elioo3g 6325  snunioolem 6355  elfz2t 6412  fzshftralt 6462  sq11 6565  dffsum 6944  caucvg3t 7112  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  ivthlem7 7230  ivthlem7OLD 7239  tpsex 7555  istps 7556  bastop2 7593  islp2 7697  iscn 7708  iscnp 7710  ismsg 7750  metxp 7786  cncfmet 7857  bl2ioo 7863  iscau 7888  lmclim 7914  isring 8093  isvclem 8148  isnvlem 8181  isphg 8420  isph 8425  phoeqi 8462  spwval 8600  spwnex 8602  shftefif1olem 8680  hhph 8984  sh2 9030  chocuni 9111  projlem15 9139  pjtheu2 9188  adjeqt 9798  elunop2t 9876  lnophmt 9882  cnlnadjeu 9948  adjbd1o 9956  jp 10135  mddmd 10173  chrelat 10228  chrelat2 10229  cvexchlem 10232  dmdbr5at 10284  cdjreu 10293  cdj3 10302  ficli 10404  cnvhmph 10450  homcard 10462  fgsb 10480  fgsb2 10485  cnfilca 10487  ismgra 10522  isalg 10533  isded 10549  iscat 10567  ishgrag 10641  ispgrag 10651
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain