Theorem syl5ibr 155

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem syl5ibr

Step	Hyp	Ref	Expression
1		syl5ibr.1	. 2 ⊢ (𝜑 → 𝜃)
2		syl5ibr.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 140	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	syl5ib 153	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:  syl5ibrcom  156  biimprd  157  nbn2  686  limelon  4321  eldifpw  4398  ssonuni  4404  onsucuni2  4479  peano2  4509  limom  4527  elrnmpt1  4790  cnveqb  4994  cnveq0  4995  relcoi1  5070  ndmfvg  5452  ffvresb  5583  caovord3d  5941  poxp  6129  nnm0r  6375  nnacl  6376  nnacom  6380  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  nnmcom  6385  brecop  6519  ecopovtrn  6526  ecopovtrng  6529  elpm2r  6560  map0g  6582  fundmen  6700  mapxpen  6742  phpm  6759  f1vrnfibi  6833  elfir  6861  mulcmpblnq  7176  ordpipqqs  7182  mulcmpblnq0  7252  genpprecll  7322  genppreclu  7323  addcmpblnr  7547  ax1rid  7685  axpre-mulgt0  7695  cnegexlem1  7937  msqge0  8378  mulge0  8381  ltleap  8394  nnmulcl  8741  nnsub  8759  elnn0z  9067  ztri3or0  9096  nneoor  9153  uz11  9348  xltnegi  9618  frec2uzuzd  10175  seq3fveq2  10242  seq3shft2  10246  seq3split  10252  seq3caopr3  10254  seq3id2  10282  seq3homo  10283  m1expcl2  10315  expadd  10335  expmul  10338  faclbnd  10487  hashfzp1  10570  hashfacen  10579  seq3coll  10585  caucvgrelemcau  10752  recan  10881  rexanre  10992  fsumiun  11246  efexp  11388  dvdstr  11530  alzdvds  11552  zob  11588  gcdmultiplez  11709  dvdssq  11719  cncongr2  11785  elrestr  12128  restopn2  12352  txcn  12444  txlm  12448  isxms2  12621  bj-om  13135  bj-inf2vnlem2  13169  bj-inf2vn  13172  bj-inf2vn2  13173