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  4446  eldifpw  4524  ssonuni  4536  onsucuni2  4612  peano2  4643  limom  4662  elrnmpt1  4929  cnveqb  5138  cnveq0  5139  relcoi1  5214  ndmfvg  5607  ffvresb  5743  caovord3d  6117  poxp  6318  nnm0r  6565  nnacl  6566  nnacom  6570  nnaass  6571  nndi  6572  nnmass  6573  nnmsucr  6574  nnmcom  6575  brecop  6712  ecopovtrn  6719  ecopovtrng  6722  elpm2r  6753  map0g  6775  fundmen  6898  mapxpen  6945  phpm  6962  f1vrnfibi  7047  elfir  7075  mulcmpblnq  7481  ordpipqqs  7487  mulcmpblnq0  7557  genpprecll  7627  genppreclu  7628  addcmpblnr  7852  ax1rid  7990  axpre-mulgt0  8000  cnegexlem1  8247  msqge0  8689  mulge0  8692  ltleap  8705  nnmulcl  9057  nnsub  9075  elnn0z  9385  ztri3or0  9414  nneoor  9475  uz11  9671  xltnegi  9957  frec2uzuzd  10547  seq3fveq2  10620  seqfveq2g  10622  seq3shft2  10626  seqshft2g  10627  seq3split  10633  seqsplitg  10634  seq3caopr3  10636  seqcaopr3g  10637  seqf1oglem2a  10663  seq3id2  10671  seq3homo  10672  seqhomog  10675  m1expcl2  10706  expadd  10726  expmul  10729  faclbnd  10886  hashfzp1  10969  hashfacen  10981  seq3coll  10987  wrdsymb0  11026  len0nnbi  11028  caucvgrelemcau  11291  recan  11420  rexanre  11531  fsumiun  11788  efexp  11993  dvdstr  12139  alzdvds  12165  zob  12202  bitsinv1  12273  gcdmultiplez  12342  dvdssq  12352  cncongr2  12426  prmdiveq  12558  pythagtriplem2  12589  pcexp  12632  elrestr  13079  ptex  13096  xpsff1o  13181  dfgrp3me  13432  mulgneg2  13492  mulgnnass  13493  mhmmulg  13499  rngpropd  13717  ringadd2  13789  mulgass2  13820  opprrngbg  13840  opprsubrngg  13973  subrngpropd  13978  subrgpropd  14015  rhmpropd  14016  lmodprop2d  14110  cnfldmulg  14338  cnfldexp  14339  restopn2  14655  txcn  14747  txlm  14751  isxms2  14924  rpcxpmul2  15385  gausslemma2dlem0i  15534  bj-om  15873  bj-inf2vnlem2  15907  bj-inf2vn  15910  bj-inf2vn2  15911