Theorem syl5ibrcom 157

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

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibrcom

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

Syntax hints:   → wi 4   ↔ wb 105

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimprcd  160  elsn2g  3702  preqr1g  3849  opth1  4328  euotd  4347  tz7.2  4451  reusv3  4557  alxfr  4558  reuhypd  4568  ordsucim  4598  suc11g  4655  nlimsucg  4664  xpsspw  4838  funcnvuni  5399  fvmptdv2  5736  fsn  5819  fconst2g  5869  funfvima  5886  foco2  5894  isores3  5956  riotaeqimp  5996  eusvobj2  6004  ovmpodv2  6155  ovelrn  6171  f1opw2  6229  suppssfv  6231  suppssov1  6232  nnmordi  6684  nnmord  6685  qsss  6763  eroveu  6795  th3qlem1  6806  mapsncnv  6864  elixpsn  6904  ixpsnf1o  6905  en1bg  6974  pw2f1odclem  7020  mapxpen  7034  en1eqsnbi  7148  updjud  7281  addnidpig  7556  enq0tr  7654  prcdnql  7704  prcunqu  7705  genipv  7729  genpelvl  7732  genpelvu  7733  distrlem5prl  7806  distrlem5pru  7807  aptiprlemu  7860  mulrid  8176  ltne  8264  cnegex  8357  creur  9139  creui  9140  cju  9141  nnsub  9182  un0addcl  9435  un0mulcl  9436  zaddcl  9519  elz2  9551  qmulz  9857  qre  9859  qnegcl  9870  elpqb  9884  xrltne  10048  xlesubadd  10118  iccid  10160  fzsn  10301  fzsuc2  10314  fz1sbc  10331  elfzp12  10334  modqmuladd  10629  bcval5  11026  bcpasc  11029  hashprg  11073  hashfzo  11087  wrdl1s1  11211  cats1un  11306  swrdccat3blem  11324  shftlem  11381  replim  11424  sqrtsq  11609  absle  11654  maxabslemval  11773  negfi  11793  xrmaxiflemval  11815  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3  11953  fsummulc2  12014  fsum00  12028  isumsplit  12057  prodmodclem2  12143  prodmodc  12144  zproddc  12145  fprodseq  12149  prodsnf  12158  fzo0dvdseq  12423  divalgmod  12493  gcdabs1  12565  dvdsgcd  12588  dvdsmulgcd  12601  lcmgcdeq  12660  isprm2lem  12693  dvdsprime  12699  coprm  12721  prmdvdsexpr  12727  rpexp  12730  phibndlem  12793  dfphi2  12797  hashgcdlem  12815  odzdvds  12823  nnoddn2prm  12838  pythagtriplem1  12843  pceulem  12872  pcqmul  12881  pcqcl  12884  pcxnn0cl  12888  pcxcl  12889  pcneg  12903  pcabs  12904  pcgcd1  12906  pcz  12910  pcprmpw2  12911  pcprmpw  12912  dvdsprmpweqle  12915  difsqpwdvds  12916  pcaddlem  12917  pcadd  12918  pcmpt  12921  pockthg  12935  4sqlem2  12967  4sqlem4  12970  mul4sq  12972  mnd1id  13544  0subm  13572  mulgnn0p1  13725  mulgnn0ass  13750  dvreq1  14162  nzrunit  14208  rrgeq0  14285  domneq0  14292  lmodfopnelem2  14345  lss1d  14403  lspsneq0  14446  znidom  14677  znunit  14679  znrrg  14680  istopon  14743  eltg3  14787  tgidm  14804  restbasg  14898  tgrest  14899  tgcn  14938  cnconst  14964  lmss  14976  txbas  14988  txbasval  14997  upxp  15002  blssps  15157  blss  15158  metrest  15236  blssioo  15283  elcncf1di  15309  elply2  15465  plyf  15467  dvdsppwf1o  15719  perfectlem2  15730  perfect  15731  lgsmod  15761  lgsne0  15773  lgsdirnn0  15782  gausslemma2dlem1a  15793  gausslemma2dlem6  15802  lgseisenlem2  15806  lgsquadlem1  15812  lgsquadlem2  15813  2lgslem1b  15824  2sqlem2  15850  mul2sq  15851  2sqlem7  15856  lpvtx  15936  usgredgop  16030  uhgrspansubgrlem  16133  vtxd0nedgbfi  16156  wlk1walkdom  16216  upgrwlkvtxedg  16221  clwwlkext2edg  16279  clwwlknonccat  16290  bj-peano4  16576