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  3589  preqr1g  3725  opth1  4191  euotd  4209  tz7.2  4309  reusv3  4414  alxfr  4415  reuhypd  4425  ordsucim  4453  suc11g  4510  nlimsucg  4519  xpsspw  4691  funcnvuni  5232  fvmptdv2  5550  fsn  5632  fconst2g  5675  funfvima  5689  foco2  5695  isores3  5756  eusvobj2  5800  ovmpodv2  5944  ovelrn  5959  f1opw2  6016  suppssfv  6018  suppssov1  6019  nnmordi  6452  nnmord  6453  qsss  6528  eroveu  6560  th3qlem1  6571  mapsncnv  6629  elixpsn  6669  ixpsnf1o  6670  en1bg  6734  mapxpen  6782  en1eqsnbi  6882  updjud  7012  addnidpig  7235  enq0tr  7333  prcdnql  7383  prcunqu  7384  genipv  7408  genpelvl  7411  genpelvu  7412  distrlem5prl  7485  distrlem5pru  7486  aptiprlemu  7539  mulid1  7854  ltne  7941  cnegex  8032  creur  8809  creui  8810  cju  8811  nnsub  8851  un0addcl  9102  un0mulcl  9103  zaddcl  9186  elz2  9214  qmulz  9510  qre  9512  qnegcl  9523  elpqb  9536  xrltne  9695  xlesubadd  9765  iccid  9807  fzsn  9946  fzsuc2  9959  fz1sbc  9976  elfzp12  9979  modqmuladd  10243  bcval5  10614  bcpasc  10617  hashprg  10659  hashfzo  10673  shftlem  10693  replim  10736  sqrtsq  10921  absle  10966  maxabslemval  11085  negfi  11104  xrmaxiflemval  11124  summodclem2  11256  summodc  11257  zsumdc  11258  fsum3  11261  fsummulc2  11322  fsum00  11336  isumsplit  11365  prodmodclem2  11451  prodmodc  11452  zproddc  11453  fprodseq  11457  prodsnf  11466  fzo0dvdseq  11722  divalgmod  11791  gcdabs1  11845  dvdsgcd  11868  dvdsmulgcd  11881  lcmgcdeq  11932  isprm2lem  11965  dvdsprime  11971  coprm  11990  prmdvdsexpr  11996  rpexp  11999  phibndlem  12060  dfphi2  12064  hashgcdlem  12078  istopon  12358  eltg3  12404  tgidm  12421  restbasg  12515  tgrest  12516  tgcn  12555  cnconst  12581  lmss  12593  txbas  12605  txbasval  12614  upxp  12619  blssps  12774  blss  12775  metrest  12853  blssioo  12892  elcncf1di  12913  bj-peano4  13476