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  11147  len0nnbi  11149  wrd2ind  11305  pfxccatin12lem2c  11312  pfxccatin12lem2  11313  swrdccatin1d  11325  caucvgrelemcau  11542  recan  11671  rexanre  11782  fsumiun  12040  efexp  12245  dvdstr  12391  alzdvds  12417  zob  12454  bitsinv1  12525  gcdmultiplez  12594  dvdssq  12604  cncongr2  12678  prmdiveq  12810  pythagtriplem2  12841  pcexp  12884  elrestr  13332  ptex  13349  xpsff1o  13434  dfgrp3me  13685  mulgneg2  13745  mulgnnass  13746  mhmmulg  13752  rngpropd  13971  ringadd2  14043  mulgass2  14074  opprrngbg  14094  opprsubrngg  14228  subrngpropd  14233  subrgpropd  14270  rhmpropd  14271  lmodprop2d  14365  cnfldmulg  14593  cnfldexp  14594  restopn2  14910  txcn  15002  txlm  15006  isxms2  15179  rpcxpmul2  15640  gausslemma2dlem0i  15789  incistruhgr  15944  upgredg2vtx  16002  upgredgpr  16003  uhgr2edg  16060  wlkres  16233  clwwlknonex2  16293  eupth2lem3lem6fi  16325  bj-om  16553  bj-inf2vnlem2  16587  bj-inf2vn  16590  bj-inf2vn2  16591