Theorem syl5ib 181

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

Hypotheses

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

Assertion

Ref	Expression
syl5ib	|- (ph -> (th -> ch))

Proof of Theorem syl5ib

Step	Hyp	Ref	Expression
1		syl5ib.1	. 2 |- (ph -> (ps -> ch))
2		syl5ib.2	. . 3 |- (th <-> ps)
3	2	biimp 133	. 2 |- (th -> ps)
4	1, 3	syl5 22	1 |- (ph -> (th -> ch))

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

This theorem is referenced by:  orel2 213  ancomsd 335  pm5.18 497  ccased 563  oplem1 578  3jao 632  19.9t 719  eqs5 832  sbequ2 864  mo 1020  r19.23ad 1285  r19.23adv 1286  rax4 1471  disjsn 1836  sssn 1852  prss 1854  tpss 1855  prel12 1875  intss1 1979  intmin 1982  iinss 2025  trel3 2049  trin 2051  ssopab2 2119  po3nr 2136  frirr 2176  fr2nr 2177  fr3nr 2178  dfwe2 2187  wefrc 2195  onfr 2237  tfis2f 2246  ssorduni 2249  onmindif 2312  onmindif2 2313  tfinds2 2405  tfinds3 2406  brrelex 2446  brelg 2458  relss 2480  funssres 2698  funun 2700  funcnvuni 2706  fv3 2839  fvelima 2859  cleqfv 2880  funopfv 2886  fopab2 2891  fvclss 2907  cbvfo 2923  isomin 2937  isofrlem 2939  f1oweOLD 2944  canth 2945  iunon 2947  iinon 2948  tfrlem1 2949  tfr3 2964  oaordi 3148  oawordeulem 3156  nnmcan 3190  omsmolem 3195  erdisj 3223  th3qlem1 3250  mapenlem2 3385  mapdom2 3389  phplem5 3407  php3 3411  fiint 3445  eirrv 3449  suc11reg 3456  trcl 3489  zfregs 3491  cplem1 3545  karden 3551  aceq3lem 3555  aceq5 3563  aceq6b 3565  ac6lem 3575  zornlem4 3606  zornlem5 3607  zornlem7 3609  fnrndomg 3617  carddom 3642  unxpdomlem 3649  alephordi 3679  alephord 3680  cfub 3703  ltmpi 3825  ltexpq 3874  ltexprlem2 3937  ltexprlem6 3941  reclem3pr 3952  reclem4pr 3953  suplem1pr 3955  mulgt0sr 4008  ssgt0sr 4011  suppsrlem 4015  suppsr2 4017  suppsr3 4018  supsr 4025  suprelem 4053  axnegex 4078  axrecex 4079  axrrecex 4081  axsup 4088  divge0 4392  nnleltp1t 4448  creur 4532  creui 4533  lt0nnn0 4549  elnn0nn 4593  sqznn 4600  uzwo 4605  nnwoOLD 4608  nn0opth 4724  infxpidmlem7 4939  infxpidmlem8 4940  infxpidmlem12 4944  infdif 4948  his6 5057  chcmh 5148  pjthu 5241  pjthu2 5242  shmods 5363  spanunsn 5482  h1datom 5483  osumlem7 5536  stm1r 5685  atcvat4 5775  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

metamath.org