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  4329  eldifpw  4406  ssonuni  4412  onsucuni2  4487  peano2  4517  limom  4535  elrnmpt1  4798  cnveqb  5002  cnveq0  5003  relcoi1  5078  ndmfvg  5460  ffvresb  5591  caovord3d  5949  poxp  6137  nnm0r  6383  nnacl  6384  nnacom  6388  nnaass  6389  nndi  6390  nnmass  6391  nnmsucr  6392  nnmcom  6393  brecop  6527  ecopovtrn  6534  ecopovtrng  6537  elpm2r  6568  map0g  6590  fundmen  6708  mapxpen  6750  phpm  6767  f1vrnfibi  6841  elfir  6869  mulcmpblnq  7200  ordpipqqs  7206  mulcmpblnq0  7276  genpprecll  7346  genppreclu  7347  addcmpblnr  7571  ax1rid  7709  axpre-mulgt0  7719  cnegexlem1  7961  msqge0  8402  mulge0  8405  ltleap  8418  nnmulcl  8765  nnsub  8783  elnn0z  9091  ztri3or0  9120  nneoor  9177  uz11  9372  xltnegi  9648  frec2uzuzd  10206  seq3fveq2  10273  seq3shft2  10277  seq3split  10283  seq3caopr3  10285  seq3id2  10313  seq3homo  10314  m1expcl2  10346  expadd  10366  expmul  10369  faclbnd  10519  hashfzp1  10602  hashfacen  10611  seq3coll  10617  caucvgrelemcau  10784  recan  10913  rexanre  11024  fsumiun  11278  efexp  11425  dvdstr  11566  alzdvds  11588  zob  11624  gcdmultiplez  11745  dvdssq  11755  cncongr2  11821  elrestr  12167  restopn2  12391  txcn  12483  txlm  12487  isxms2  12660  bj-om  13306  bj-inf2vnlem2  13340  bj-inf2vn  13343  bj-inf2vn2  13344