Theorem syl6bb 414

Description: A syllogism inference from two biconditionals.

Hypotheses

Ref	Expression
syl6bb.1	|- (ph -> (ps <-> ch))
syl6bb.2	|- (ch <-> th)

Assertion

Ref	Expression
syl6bb	|- (ph -> (ps <-> th))

Proof of Theorem syl6bb

Step	Hyp	Ref	Expression
1		syl6bb.1	. 2 |- (ph -> (ps <-> ch))
2		syl6bb.2	. . 3 |- (ch <-> th)
3	2	a1i 7	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 406	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 2   <-> wb 127

This theorem is referenced by:  syl6rbb 415  syl6bbr 416  3bitr3g 427  biantrurd 546  19.33b 771  eqsal 833  axac 1085  cleqabd 1178  eqvinc 1407  eueq3 1430  reuxfr 1580  moabex 1868  eluniab 1926  elintab 1976  sotrieq2 2150  ordtri2 2233  ordtri4 2235  oneqmini 2272  ordtri2or 2328  ralxp 2456  opelcog 2511  opelcnvg 2517  dmsnop 2547  reldm0 2550  relrn0 2568  iss 2599  fvprc 2829  fnfvop 2856  fvopab3 2868  fvopabn 2873  elrnopab 2884  fsn 2895  fconstfv 2903  f1fv 2916  isocnv 2934  isoini 2938  f1oiso 2942  eloprabg 3035  elrnoprab 3054  caoprord2 3071  ecopoprsym 3246  th3qlem1 3250  dom2d 3307  mapsnen 3334  undom 3342  xpdom2 3345  pw2en 3348  mapdom2 3389  mapxpen 3390  xpmapenlem5 3395  unfilem1 3438  inf3lem1 3464  r1tr 3498  rankval2 3514  rankr1 3518  rankval3 3525  unbndrank 3527  r1pwcl 3530  bnd2 3549  aceq0 3553  aceq5lem4 3561  aceq5 3563  ac6lem 3575  kmlem14 3593  iscard2 3660  alephord2 3681  cardaleph 3690  zfcndac 3765  ltexpi 3823  mulcmpblnq 3847  ordpipq 3850  ltsopq 3869  genpelv 3897  genpprecl 3898  genpnnp 3902  genpass 3906  distrlem1pr 3921  distrlem5pr 3925  prlem936a 3947  addcmpblnr 3975  ltsrpr 3980  ltsosr 3997  mulgt0sr 4008  map2psrpr 4014  ltresr 4052  axrnegex 4080  axrrecex 4081  axltadd 4085  axmulgt0 4086  negcon2t 4168  lt0neg1t 4370  lt0neg2t 4371  le0neg1t 4372  le0neg2t 4373  ltmul2 4395  lemul1 4397  nngt1ne1t 4440  arch 4521  creur 4532  creui 4533  nn0ltp1let 4556  elznn0 4576  elnnz1 4581  elnn0nn 4593  zltp1let 4597  uzwo3lem2 4615  seqlem2 4663  sqr2irrlem3 4779  xpnnen 4927  infxpidmlem5 4937  infxpidmlem10 4942  ocelt 5162  ocsh 5164  chocuni 5179  shselt 5280  shscomt 5284  shmods 5363  elspan 5449  large 5700  mdbr2 5728  chrelat3t 5762  atnem0 5766  sumdmdi 5785  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org