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  3617  preqr1g  3754  opth1  4222  euotd  4240  tz7.2  4340  reusv3  4446  alxfr  4447  reuhypd  4457  ordsucim  4485  suc11g  4542  nlimsucg  4551  xpsspw  4724  funcnvuni  5269  fvmptdv2  5589  fsn  5672  fconst2g  5715  funfvima  5731  foco2  5737  isores3  5798  eusvobj2  5843  ovmpodv2  5990  ovelrn  6005  f1opw2  6059  suppssfv  6061  suppssov1  6062  nnmordi  6499  nnmord  6500  qsss  6576  eroveu  6608  th3qlem1  6619  mapsncnv  6677  elixpsn  6717  ixpsnf1o  6718  en1bg  6782  mapxpen  6830  en1eqsnbi  6930  updjud  7063  addnidpig  7302  enq0tr  7400  prcdnql  7450  prcunqu  7451  genipv  7475  genpelvl  7478  genpelvu  7479  distrlem5prl  7552  distrlem5pru  7553  aptiprlemu  7606  mulid1  7921  ltne  8008  cnegex  8101  creur  8879  creui  8880  cju  8881  nnsub  8921  un0addcl  9172  un0mulcl  9173  zaddcl  9256  elz2  9287  qmulz  9586  qre  9588  qnegcl  9599  elpqb  9612  xrltne  9774  xlesubadd  9844  iccid  9886  fzsn  10026  fzsuc2  10039  fz1sbc  10056  elfzp12  10059  modqmuladd  10326  bcval5  10701  bcpasc  10704  hashprg  10747  hashfzo  10761  shftlem  10784  replim  10827  sqrtsq  11012  absle  11057  maxabslemval  11176  negfi  11195  xrmaxiflemval  11217  summodclem2  11349  summodc  11350  zsumdc  11351  fsum3  11354  fsummulc2  11415  fsum00  11429  isumsplit  11458  prodmodclem2  11544  prodmodc  11545  zproddc  11546  fprodseq  11550  prodsnf  11559  fzo0dvdseq  11821  divalgmod  11890  gcdabs1  11948  dvdsgcd  11971  dvdsmulgcd  11984  lcmgcdeq  12041  isprm2lem  12074  dvdsprime  12080  coprm  12102  prmdvdsexpr  12108  rpexp  12111  phibndlem  12174  dfphi2  12178  hashgcdlem  12196  odzdvds  12203  nnoddn2prm  12218  pythagtriplem1  12223  pceulem  12252  pcqmul  12261  pcqcl  12264  pcxnn0cl  12268  pcxcl  12269  pcneg  12282  pcabs  12283  pcgcd1  12285  pcz  12289  pcprmpw2  12290  pcprmpw  12291  dvdsprmpweqle  12294  difsqpwdvds  12295  pcaddlem  12296  pcadd  12297  pcmpt  12299  pockthg  12313  4sqlem2  12345  4sqlem4  12348  mul4sq  12350  mnd1id  12684  0subm  12706  mulgnn0p1  12827  mulgnn0ass  12851  istopon  12890  eltg3  12936  tgidm  12953  restbasg  13047  tgrest  13048  tgcn  13087  cnconst  13113  lmss  13125  txbas  13137  txbasval  13146  upxp  13151  blssps  13306  blss  13307  metrest  13385  blssioo  13424  elcncf1di  13445  lgsmod  13806  lgsne0  13818  lgsdirnn0  13827  2sqlem2  13830  mul2sq  13831  2sqlem7  13836  bj-peano4  14075