Theorem syl5ibrcom 156

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 155	. 2 ⊢ (𝜒 → (𝜑 → 𝜓))
4	3	com12 30	1 ⊢ (𝜑 → (𝜒 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimprcd  159  elsn2g  3565  preqr1g  3701  opth1  4166  euotd  4184  tz7.2  4284  reusv3  4389  alxfr  4390  reuhypd  4400  ordsucim  4424  suc11g  4480  nlimsucg  4489  xpsspw  4659  funcnvuni  5200  fvmptdv2  5518  fsn  5600  fconst2g  5643  funfvima  5657  foco2  5663  isores3  5724  eusvobj2  5768  ovmpodv2  5912  ovelrn  5927  f1opw2  5984  suppssfv  5986  suppssov1  5987  nnmordi  6420  nnmord  6421  qsss  6496  eroveu  6528  th3qlem1  6539  mapsncnv  6597  elixpsn  6637  ixpsnf1o  6638  en1bg  6702  mapxpen  6750  en1eqsnbi  6845  updjud  6975  addnidpig  7168  enq0tr  7266  prcdnql  7316  prcunqu  7317  genipv  7341  genpelvl  7344  genpelvu  7345  distrlem5prl  7418  distrlem5pru  7419  aptiprlemu  7472  mulid1  7787  ltne  7873  cnegex  7964  creur  8741  creui  8742  cju  8743  nnsub  8783  un0addcl  9034  un0mulcl  9035  zaddcl  9118  elz2  9146  qmulz  9442  qre  9444  qnegcl  9455  elpqb  9468  xrltne  9626  xlesubadd  9696  iccid  9738  fzsn  9877  fzsuc2  9890  fz1sbc  9907  elfzp12  9910  modqmuladd  10170  bcval5  10541  bcpasc  10544  hashprg  10586  hashfzo  10600  shftlem  10620  replim  10663  sqrtsq  10848  absle  10893  maxabslemval  11012  negfi  11031  xrmaxiflemval  11051  summodclem2  11183  summodc  11184  zsumdc  11185  fsum3  11188  fsummulc2  11249  fsum00  11263  isumsplit  11292  prodmodclem2  11378  prodmodc  11379  zproddc  11380  fprodseq  11384  fzo0dvdseq  11591  divalgmod  11660  gcdabs1  11713  dvdsgcd  11736  dvdsmulgcd  11749  lcmgcdeq  11800  isprm2lem  11833  dvdsprime  11839  coprm  11858  prmdvdsexpr  11864  rpexp  11867  phibndlem  11928  dfphi2  11932  hashgcdlem  11939  istopon  12219  eltg3  12265  tgidm  12282  restbasg  12376  tgrest  12377  tgcn  12416  cnconst  12442  lmss  12454  txbas  12466  txbasval  12475  upxp  12480  blssps  12635  blss  12636  metrest  12714  blssioo  12753  elcncf1di  12774  bj-peano4  13324