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-1 5  ax-2 6  ax-mp 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  651  limelon  4250  eldifpw  4327  ssonuni  4333  onsucuni2  4408  peano2  4438  limom  4456  elrnmpt1  4718  cnveqb  4920  cnveq0  4921  relcoi1  4996  ndmfvg  5370  ffvresb  5500  caovord3d  5853  poxp  6035  nnm0r  6280  nnacl  6281  nnacom  6285  nnaass  6286  nndi  6287  nnmass  6288  nnmsucr  6289  nnmcom  6290  brecop  6422  ecopovtrn  6429  ecopovtrng  6432  elpm2r  6463  map0g  6485  fundmen  6603  mapxpen  6644  phpm  6661  f1vrnfibi  6734  mulcmpblnq  7024  ordpipqqs  7030  mulcmpblnq0  7100  genpprecll  7170  genppreclu  7171  addcmpblnr  7382  ax1rid  7509  axpre-mulgt0  7519  cnegexlem1  7754  msqge0  8190  mulge0  8193  ltleap  8204  nnmulcl  8541  nnsub  8559  elnn0z  8861  ztri3or0  8890  nneoor  8947  uz11  9140  xltnegi  9401  frec2uzuzd  9958  iseqsst  10031  seq3fveq2  10034  seq3shft2  10038  seq3split  10045  seq3caopr3  10047  seq3id2  10075  seq3homo  10076  m1expcl2  10108  expadd  10128  expmul  10131  faclbnd  10280  hashfzp1  10363  hashfacen  10372  seq3coll  10378  caucvgrelemcau  10544  recan  10673  rexanre  10784  fsumiun  11035  efexp  11136  dvdstr  11275  alzdvds  11297  zob  11333  gcdmultiplez  11452  dvdssq  11462  cncongr2  11528  elrestr  11827  restopn2  12050  isxms2  12253  bj-om  12544  bj-inf2vnlem2  12578  bj-inf2vn  12581  bj-inf2vn2  12582