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  704  anifpdc  994  limelon  4496  eldifpw  4574  ssonuni  4586  onsucuni2  4662  peano2  4693  limom  4712  elrnmpt1  4983  cnveqb  5192  cnveq0  5193  relcoi1  5268  f1ssf1  5615  ndmfvg  5670  ffvresb  5810  caovord3d  6193  poxp  6397  nnm0r  6647  nnacl  6648  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  brecop  6794  ecopovtrn  6801  ecopovtrng  6804  elpm2r  6835  map0g  6857  fundmen  6981  dom1o  7002  mapxpen  7034  phpm  7052  f1vrnfibi  7144  elfir  7172  mulcmpblnq  7588  ordpipqqs  7594  mulcmpblnq0  7664  genpprecll  7734  genppreclu  7735  addcmpblnr  7959  ax1rid  8097  axpre-mulgt0  8107  cnegexlem1  8354  msqge0  8796  mulge0  8799  ltleap  8812  nnmulcl  9164  nnsub  9182  elnn0z  9492  ztri3or0  9521  nneoor  9582  uz11  9779  xltnegi  10070  frec2uzuzd  10665  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seqf1oglem2a  10781  seq3id2  10789  seq3homo  10790  seqhomog  10793  m1expcl2  10824  expadd  10844  expmul  10847  faclbnd  11004  hashfzp1  11089  hashfacen  11101  seq3coll  11107  wrdsymb0  11150  len0nnbi  11152  wrd2ind  11308  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  swrdccatin1d  11328  caucvgrelemcau  11545  recan  11674  rexanre  11785  fsumiun  12043  efexp  12248  dvdstr  12394  alzdvds  12420  zob  12457  bitsinv1  12528  gcdmultiplez  12597  dvdssq  12607  cncongr2  12681  prmdiveq  12813  pythagtriplem2  12844  pcexp  12887  elrestr  13335  ptex  13352  xpsff1o  13437  dfgrp3me  13688  mulgneg2  13748  mulgnnass  13749  mhmmulg  13755  rngpropd  13974  ringadd2  14046  mulgass2  14077  opprrngbg  14097  opprsubrngg  14231  subrngpropd  14236  subrgpropd  14273  rhmpropd  14274  lmodprop2d  14368  cnfldmulg  14596  cnfldexp  14597  restopn2  14913  txcn  15005  txlm  15009  isxms2  15182  rpcxpmul2  15643  gausslemma2dlem0i  15792  incistruhgr  15947  upgredg2vtx  16005  upgredgpr  16006  uhgr2edg  16063  wlkres  16236  clwwlknonex2  16296  eupth2lem3lem6fi  16328  bj-om  16558  bj-inf2vnlem2  16592  bj-inf2vn  16595  bj-inf2vn2  16596