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  687  limelon  4376  eldifpw  4454  ssonuni  4464  onsucuni2  4540  peano2  4571  limom  4590  elrnmpt1  4854  cnveqb  5058  cnveq0  5059  relcoi1  5134  ndmfvg  5516  ffvresb  5647  caovord3d  6008  poxp  6196  nnm0r  6443  nnacl  6444  nnacom  6448  nnaass  6449  nndi  6450  nnmass  6451  nnmsucr  6452  nnmcom  6453  brecop  6587  ecopovtrn  6594  ecopovtrng  6597  elpm2r  6628  map0g  6650  fundmen  6768  mapxpen  6810  phpm  6827  f1vrnfibi  6906  elfir  6934  mulcmpblnq  7305  ordpipqqs  7311  mulcmpblnq0  7381  genpprecll  7451  genppreclu  7452  addcmpblnr  7676  ax1rid  7814  axpre-mulgt0  7824  cnegexlem1  8069  msqge0  8510  mulge0  8513  ltleap  8526  nnmulcl  8874  nnsub  8892  elnn0z  9200  ztri3or0  9229  nneoor  9289  uz11  9484  xltnegi  9767  frec2uzuzd  10333  seq3fveq2  10400  seq3shft2  10404  seq3split  10410  seq3caopr3  10412  seq3id2  10440  seq3homo  10441  m1expcl2  10473  expadd  10493  expmul  10496  faclbnd  10650  hashfzp1  10733  hashfacen  10745  seq3coll  10751  caucvgrelemcau  10918  recan  11047  rexanre  11158  fsumiun  11414  efexp  11619  dvdstr  11764  alzdvds  11788  zob  11824  gcdmultiplez  11950  dvdssq  11960  cncongr2  12032  prmdiveq  12164  pythagtriplem2  12194  pcexp  12237  elrestr  12559  restopn2  12783  txcn  12875  txlm  12879  isxms2  13052  bj-om  13779  bj-inf2vnlem2  13813  bj-inf2vn  13816  bj-inf2vn2  13817