Theorem imbitrrid 156

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

Hypotheses

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

Assertion

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

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 141	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 154	1 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibrcom  157  biimprd  158  nbn2  698  limelon  4435  eldifpw  4513  ssonuni  4525  onsucuni2  4601  peano2  4632  limom  4651  elrnmpt1  4918  cnveqb  5126  cnveq0  5127  relcoi1  5202  ndmfvg  5590  ffvresb  5726  caovord3d  6095  poxp  6291  nnm0r  6538  nnacl  6539  nnacom  6543  nnaass  6544  nndi  6545  nnmass  6546  nnmsucr  6547  nnmcom  6548  brecop  6685  ecopovtrn  6692  ecopovtrng  6695  elpm2r  6726  map0g  6748  fundmen  6866  mapxpen  6910  phpm  6927  f1vrnfibi  7012  elfir  7040  mulcmpblnq  7437  ordpipqqs  7443  mulcmpblnq0  7513  genpprecll  7583  genppreclu  7584  addcmpblnr  7808  ax1rid  7946  axpre-mulgt0  7956  cnegexlem1  8203  msqge0  8645  mulge0  8648  ltleap  8661  nnmulcl  9013  nnsub  9031  elnn0z  9341  ztri3or0  9370  nneoor  9430  uz11  9626  xltnegi  9912  frec2uzuzd  10496  seq3fveq2  10569  seqfveq2g  10571  seq3shft2  10575  seqshft2g  10576  seq3split  10582  seqsplitg  10583  seq3caopr3  10585  seqcaopr3g  10586  seqf1oglem2a  10612  seq3id2  10620  seq3homo  10621  seqhomog  10624  m1expcl2  10655  expadd  10675  expmul  10678  faclbnd  10835  hashfzp1  10918  hashfacen  10930  seq3coll  10936  wrdsymb0  10969  len0nnbi  10971  caucvgrelemcau  11147  recan  11276  rexanre  11387  fsumiun  11644  efexp  11849  dvdstr  11995  alzdvds  12021  zob  12058  bitsinv1  12129  gcdmultiplez  12198  dvdssq  12208  cncongr2  12282  prmdiveq  12414  pythagtriplem2  12445  pcexp  12488  elrestr  12928  ptex  12945  xpsff1o  13002  dfgrp3me  13242  mulgneg2  13296  mulgnnass  13297  mhmmulg  13303  rngpropd  13521  ringadd2  13593  mulgass2  13624  opprrngbg  13644  opprsubrngg  13777  subrngpropd  13782  subrgpropd  13819  rhmpropd  13820  lmodprop2d  13914  cnfldmulg  14142  cnfldexp  14143  restopn2  14429  txcn  14521  txlm  14525  isxms2  14698  rpcxpmul2  15159  gausslemma2dlem0i  15308  bj-om  15593  bj-inf2vnlem2  15627  bj-inf2vn  15630  bj-inf2vn2  15631