Theorem syl5ibrcom 155

Description: A mixed syllogism inference. (Contributed by NM, 20-Jun-2007.)

Hypotheses

Ref	Expression
syl5ibr.1	⊢ (𝜑 → 𝜃)
syl5ibr.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
syl5ibrcom	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem syl5ibrcom

Step	Hyp	Ref	Expression
1		syl5ibr.1	. . 3 ⊢ (𝜑 → 𝜃)
2		syl5ibr.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	1, 2	syl5ibr 154	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 30	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  biimprcd  158  elsn2g  3427  preqr1g  3558  opth1  3991  euotd  4009  tz7.2  4109  reusv3  4210  alxfr  4211  reuhypd  4221  ordsucim  4244  suc11g  4300  nlimsucg  4309  xpsspw  4468  funcnvuni  4988  fvmptdv2  5281  foco2  5339  fsn  5356  fconst2g  5397  funfvima  5411  isores3  5475  eusvobj2  5518  ovmpt2dv2  5654  ovelrn  5669  f1opw2  5726  suppssfv  5728  suppssov1  5729  nnmordi  6112  nnmord  6113  qsss  6188  eroveu  6220  th3qlem1  6231  en1bg  6303  addnidpig  6526  enq0tr  6624  prcdnql  6674  prcunqu  6675  genipv  6699  genpelvl  6702  genpelvu  6703  distrlem5prl  6776  distrlem5pru  6777  aptiprlemu  6830  mulid1  7116  ltne  7196  cnegex  7286  creur  8036  creui  8037  cju  8038  nnsub  8077  un0addcl  8321  un0mulcl  8322  zaddcl  8391  elz2  8419  qmulz  8708  qre  8710  qnegcl  8721  xrltne  8883  iccid  8948  fzsn  9084  fzsuc2  9096  fz1sbc  9113  elfzp12  9116  modqmuladd  9368  iseqid3  9465  ibcval5  9690  bcpasc  9693  shftlem  9704  replim  9746  sqrtsq  9930  absle  9975  maxabslemval  10094  negfi  10110  fzo0dvdseq  10257  divalgmod  10327  gcdabs1  10380  dvdsgcd  10401  dvdsmulgcd  10414  lcmgcdeq  10465  isprm2lem  10498  dvdsprime  10504  coprm  10523  prmdvdsexpr  10529  rpexp  10532  bj-peano4  10750