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  3558  preqr1g  3693  opth1  4158  euotd  4176  tz7.2  4276  reusv3  4381  alxfr  4382  reuhypd  4392  ordsucim  4416  suc11g  4472  nlimsucg  4481  xpsspw  4651  funcnvuni  5192  fvmptdv2  5510  fsn  5592  fconst2g  5635  funfvima  5649  foco2  5655  isores3  5716  eusvobj2  5760  ovmpodv2  5904  ovelrn  5919  f1opw2  5976  suppssfv  5978  suppssov1  5979  nnmordi  6412  nnmord  6413  qsss  6488  eroveu  6520  th3qlem1  6531  mapsncnv  6589  elixpsn  6629  ixpsnf1o  6630  en1bg  6694  mapxpen  6742  en1eqsnbi  6837  updjud  6967  addnidpig  7144  enq0tr  7242  prcdnql  7292  prcunqu  7293  genipv  7317  genpelvl  7320  genpelvu  7321  distrlem5prl  7394  distrlem5pru  7395  aptiprlemu  7448  mulid1  7763  ltne  7849  cnegex  7940  creur  8717  creui  8718  cju  8719  nnsub  8759  un0addcl  9010  un0mulcl  9011  zaddcl  9094  elz2  9122  qmulz  9415  qre  9417  qnegcl  9428  xrltne  9596  xlesubadd  9666  iccid  9708  fzsn  9846  fzsuc2  9859  fz1sbc  9876  elfzp12  9879  modqmuladd  10139  bcval5  10509  bcpasc  10512  hashprg  10554  hashfzo  10568  shftlem  10588  replim  10631  sqrtsq  10816  absle  10861  maxabslemval  10980  negfi  10999  xrmaxiflemval  11019  summodclem2  11151  summodc  11152  zsumdc  11153  fsum3  11156  fsummulc2  11217  fsum00  11231  isumsplit  11260  prodmodclem2  11346  prodmodc  11347  fzo0dvdseq  11555  divalgmod  11624  gcdabs1  11677  dvdsgcd  11700  dvdsmulgcd  11713  lcmgcdeq  11764  isprm2lem  11797  dvdsprime  11803  coprm  11822  prmdvdsexpr  11828  rpexp  11831  phibndlem  11892  dfphi2  11896  hashgcdlem  11903  istopon  12180  eltg3  12226  tgidm  12243  restbasg  12337  tgrest  12338  tgcn  12377  cnconst  12403  lmss  12415  txbas  12427  txbasval  12436  upxp  12441  blssps  12596  blss  12597  metrest  12675  blssioo  12714  elcncf1di  12735  bj-peano4  13153