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  698  limelon  4431  eldifpw  4509  ssonuni  4521  onsucuni2  4597  peano2  4628  limom  4647  elrnmpt1  4914  cnveqb  5122  cnveq0  5123  relcoi1  5198  ndmfvg  5586  ffvresb  5722  caovord3d  6091  poxp  6287  nnm0r  6534  nnacl  6535  nnacom  6539  nnaass  6540  nndi  6541  nnmass  6542  nnmsucr  6543  nnmcom  6544  brecop  6681  ecopovtrn  6688  ecopovtrng  6691  elpm2r  6722  map0g  6744  fundmen  6862  mapxpen  6906  phpm  6923  f1vrnfibi  7006  elfir  7034  mulcmpblnq  7430  ordpipqqs  7436  mulcmpblnq0  7506  genpprecll  7576  genppreclu  7577  addcmpblnr  7801  ax1rid  7939  axpre-mulgt0  7949  cnegexlem1  8196  msqge0  8637  mulge0  8640  ltleap  8653  nnmulcl  9005  nnsub  9023  elnn0z  9333  ztri3or0  9362  nneoor  9422  uz11  9618  xltnegi  9904  frec2uzuzd  10476  seq3fveq2  10549  seqfveq2g  10551  seq3shft2  10555  seqshft2g  10556  seq3split  10562  seqsplitg  10563  seq3caopr3  10565  seqcaopr3g  10566  seqf1oglem2a  10592  seq3id2  10600  seq3homo  10601  seqhomog  10604  m1expcl2  10635  expadd  10655  expmul  10658  faclbnd  10815  hashfzp1  10898  hashfacen  10910  seq3coll  10916  wrdsymb0  10949  len0nnbi  10951  caucvgrelemcau  11127  recan  11256  rexanre  11367  fsumiun  11623  efexp  11828  dvdstr  11974  alzdvds  11999  zob  12035  gcdmultiplez  12161  dvdssq  12171  cncongr2  12245  prmdiveq  12377  pythagtriplem2  12407  pcexp  12450  elrestr  12861  ptex  12878  xpsff1o  12935  dfgrp3me  13175  mulgneg2  13229  mulgnnass  13230  mhmmulg  13236  rngpropd  13454  ringadd2  13526  mulgass2  13557  opprrngbg  13577  opprsubrngg  13710  subrngpropd  13715  subrgpropd  13752  rhmpropd  13753  lmodprop2d  13847  cnfldmulg  14075  cnfldexp  14076  restopn2  14362  txcn  14454  txlm  14458  isxms2  14631  gausslemma2dlem0i  15214  bj-om  15499  bj-inf2vnlem2  15533  bj-inf2vn  15536  bj-inf2vn2  15537