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  692  limelon  4384  eldifpw  4462  ssonuni  4472  onsucuni2  4548  peano2  4579  limom  4598  elrnmpt1  4862  cnveqb  5066  cnveq0  5067  relcoi1  5142  ndmfvg  5527  ffvresb  5659  caovord3d  6023  poxp  6211  nnm0r  6458  nnacl  6459  nnacom  6463  nnaass  6464  nndi  6465  nnmass  6466  nnmsucr  6467  nnmcom  6468  brecop  6603  ecopovtrn  6610  ecopovtrng  6613  elpm2r  6644  map0g  6666  fundmen  6784  mapxpen  6826  phpm  6843  f1vrnfibi  6922  elfir  6950  mulcmpblnq  7330  ordpipqqs  7336  mulcmpblnq0  7406  genpprecll  7476  genppreclu  7477  addcmpblnr  7701  ax1rid  7839  axpre-mulgt0  7849  cnegexlem1  8094  msqge0  8535  mulge0  8538  ltleap  8551  nnmulcl  8899  nnsub  8917  elnn0z  9225  ztri3or0  9254  nneoor  9314  uz11  9509  xltnegi  9792  frec2uzuzd  10358  seq3fveq2  10425  seq3shft2  10429  seq3split  10435  seq3caopr3  10437  seq3id2  10465  seq3homo  10466  m1expcl2  10498  expadd  10518  expmul  10521  faclbnd  10675  hashfzp1  10759  hashfacen  10771  seq3coll  10777  caucvgrelemcau  10944  recan  11073  rexanre  11184  fsumiun  11440  efexp  11645  dvdstr  11790  alzdvds  11814  zob  11850  gcdmultiplez  11976  dvdssq  11986  cncongr2  12058  prmdiveq  12190  pythagtriplem2  12220  pcexp  12263  elrestr  12587  restopn2  12977  txcn  13069  txlm  13073  isxms2  13246  bj-om  13972  bj-inf2vnlem2  14006  bj-inf2vn  14009  bj-inf2vn2  14010