Theorem syl6ibr 213

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition.

Hypotheses

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

Assertion

Ref	Expression
syl6ibr	|- (ph -> (ps -> th))

Proof of Theorem syl6ibr

Step	Hyp	Ref	Expression
1		syl6ibr.1	. 2 |- (ph -> (ps -> ch))
2		syl6ibr.2	. . 3 |- (th <-> ch)
3	2	biimpr 152	. 2 |- (ch -> th)
4	1, 3	syl6 22	1 |- (ph -> (ps -> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  imp4a 364  nicodraw 948  hband 1087  equs5e 1182  mopick2 1413  euor2 1414  2moswap 1421  2eu1 1426  necon3bd 1579  necon3d 1580  necon2ad 1590  r19.21ad 1693  cla4egf 1836  cla42gv 1840  ra5 1971  difsn 2434  pwpw0 2439  sssn 2443  ssuni 2490  dfwe2 2898  wefrc 2906  ordtri3or 2942  ordtri3 2946  ordon 2950  ssorduni 2956  oneqmini 2980  tfis 3090  nnsuc 3111  ssrel 3209  opeldm 3271  relssres 3343  cotr 3387  cnvsym 3388  ssrnres 3427  funss 3475  fnun 3534  f1oun 3645  ssimaex 3707  fvopab3ig 3717  chfnrn 3741  dffo4 3759  dffo5 3760  fvclss 3794  isomin 3838  isofrlem 3840  f1oweALT 3845  rdglim2 3888  tz7.48lem 3894  tz7.49 3898  fnoprabg 3951  oprabvalig 3963  infsdomnn 4463  pssnn 4465  pm54.43 4498  inf3lem4 4540  rankr1 4598  r1pwcl 4611  aceq5lem4 4662  aceq5 4664  aceq6b 4666  ac5b 4677  kmlem2 4690  zorn2lem4 4715  zorn2lem6 4717  zorn2lem7 4718  cardne 4754  carden 4755  carddom 4759  alephordi 4797  cardaleph 4808  carduniima 4813  cardinfima 4814  alephval3 4826  cflim 4832  indpi 4957  ltaddpq 5002  genpcl 5034  prlem934 5062  ltaddpr 5063  ltexprlem1 5065  ltexprlem5 5069  reclem4pr 5082  suplem1pr 5084  pre-axsup 5214  zaddclt 6063  zmulclt 6078  zneo 6098  zneoOLD 6099  uzwo4OLD 6109  icoshft 6292  uzwo 6338  uzwoOLD 6339  nn0opth 6547  sqr2irr 6610  caubnd 6814  bccl2t 6860  iserzcmp0 7030  caucvglem2 7045  basgen2t 7532  distop 7542  cnpco 7656  cncnplem2 7662  metreslem 7710  unirnbl 7763  metelcls 7848  ubthlem5 8399  oprabvaligg 8700  cdrci 8738  fipfil 8788  fipfil2 8789  filintf 8793  rdmob 8875  shmods 9491  orthin 9499  spansneleqOLD 9624  h1datom 9635  osumlem4 9712  stcltr2 10326  atom1d 10402  sumdmdi 10463  cdj3lem1 10480

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

Copyright terms: Public domain