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	|- ( ph -> th )
imbitrrid.2	|- ( ch -> ( ps <-> th ) )

Assertion

Ref	Expression
imbitrrid	|- ( ch -> ( ph -> ps ) )

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 |- ( ph -> th )
2		imbitrrid.2	. . 3 |- ( ch -> ( ps <-> th ) )
3	2	bicomd 141	. 2 |- ( ch -> ( th <-> ps ) )
4	1, 3	imbitrid 154	1 |- ( ch -> ( ph -> ps ) )

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  699  limelon  4464  eldifpw  4542  ssonuni  4554  onsucuni2  4630  peano2  4661  limom  4680  elrnmpt1  4948  cnveqb  5157  cnveq0  5158  relcoi1  5233  ndmfvg  5630  ffvresb  5766  caovord3d  6140  poxp  6341  nnm0r  6588  nnacl  6589  nnacom  6593  nnaass  6594  nndi  6595  nnmass  6596  nnmsucr  6597  nnmcom  6598  brecop  6735  ecopovtrn  6742  ecopovtrng  6745  elpm2r  6776  map0g  6798  fundmen  6922  mapxpen  6970  phpm  6988  f1vrnfibi  7073  elfir  7101  mulcmpblnq  7516  ordpipqqs  7522  mulcmpblnq0  7592  genpprecll  7662  genppreclu  7663  addcmpblnr  7887  ax1rid  8025  axpre-mulgt0  8035  cnegexlem1  8282  msqge0  8724  mulge0  8727  ltleap  8740  nnmulcl  9092  nnsub  9110  elnn0z  9420  ztri3or0  9449  nneoor  9510  uz11  9706  xltnegi  9992  frec2uzuzd  10584  seq3fveq2  10657  seqfveq2g  10659  seq3shft2  10663  seqshft2g  10664  seq3split  10670  seqsplitg  10671  seq3caopr3  10673  seqcaopr3g  10674  seqf1oglem2a  10700  seq3id2  10708  seq3homo  10709  seqhomog  10712  m1expcl2  10743  expadd  10763  expmul  10766  faclbnd  10923  hashfzp1  11006  hashfacen  11018  seq3coll  11024  wrdsymb0  11063  len0nnbi  11065  wrd2ind  11214  pfxccatin12lem2c  11221  pfxccatin12lem2  11222  swrdccatin1d  11234  caucvgrelemcau  11406  recan  11535  rexanre  11646  fsumiun  11903  efexp  12108  dvdstr  12254  alzdvds  12280  zob  12317  bitsinv1  12388  gcdmultiplez  12457  dvdssq  12467  cncongr2  12541  prmdiveq  12673  pythagtriplem2  12704  pcexp  12747  elrestr  13194  ptex  13211  xpsff1o  13296  dfgrp3me  13547  mulgneg2  13607  mulgnnass  13608  mhmmulg  13614  rngpropd  13832  ringadd2  13904  mulgass2  13935  opprrngbg  13955  opprsubrngg  14088  subrngpropd  14093  subrgpropd  14130  rhmpropd  14131  lmodprop2d  14225  cnfldmulg  14453  cnfldexp  14454  restopn2  14770  txcn  14862  txlm  14866  isxms2  15039  rpcxpmul2  15500  gausslemma2dlem0i  15649  incistruhgr  15801  upgredg2vtx  15852  upgredgpr  15853  bj-om  16072  bj-inf2vnlem2  16106  bj-inf2vn  16109  bj-inf2vn2  16110  dom1o  16128