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  702  anifpdc  992  limelon  4489  eldifpw  4567  ssonuni  4579  onsucuni2  4655  peano2  4686  limom  4705  elrnmpt1  4974  cnveqb  5183  cnveq0  5184  relcoi1  5259  ndmfvg  5657  ffvresb  5797  caovord3d  6175  poxp  6376  nnm0r  6623  nnacl  6624  nnacom  6628  nnaass  6629  nndi  6630  nnmass  6631  nnmsucr  6632  nnmcom  6633  brecop  6770  ecopovtrn  6777  ecopovtrng  6780  elpm2r  6811  map0g  6833  fundmen  6957  mapxpen  7005  phpm  7023  f1vrnfibi  7108  elfir  7136  mulcmpblnq  7551  ordpipqqs  7557  mulcmpblnq0  7627  genpprecll  7697  genppreclu  7698  addcmpblnr  7922  ax1rid  8060  axpre-mulgt0  8070  cnegexlem1  8317  msqge0  8759  mulge0  8762  ltleap  8775  nnmulcl  9127  nnsub  9145  elnn0z  9455  ztri3or0  9484  nneoor  9545  uz11  9741  xltnegi  10027  frec2uzuzd  10619  seq3fveq2  10692  seqfveq2g  10694  seq3shft2  10698  seqshft2g  10699  seq3split  10705  seqsplitg  10706  seq3caopr3  10708  seqcaopr3g  10709  seqf1oglem2a  10735  seq3id2  10743  seq3homo  10744  seqhomog  10747  m1expcl2  10778  expadd  10798  expmul  10801  faclbnd  10958  hashfzp1  11041  hashfacen  11053  seq3coll  11059  wrdsymb0  11099  len0nnbi  11101  wrd2ind  11250  pfxccatin12lem2c  11257  pfxccatin12lem2  11258  swrdccatin1d  11270  caucvgrelemcau  11486  recan  11615  rexanre  11726  fsumiun  11983  efexp  12188  dvdstr  12334  alzdvds  12360  zob  12397  bitsinv1  12468  gcdmultiplez  12537  dvdssq  12547  cncongr2  12621  prmdiveq  12753  pythagtriplem2  12784  pcexp  12827  elrestr  13275  ptex  13292  xpsff1o  13377  dfgrp3me  13628  mulgneg2  13688  mulgnnass  13689  mhmmulg  13695  rngpropd  13913  ringadd2  13985  mulgass2  14016  opprrngbg  14036  opprsubrngg  14169  subrngpropd  14174  subrgpropd  14211  rhmpropd  14212  lmodprop2d  14306  cnfldmulg  14534  cnfldexp  14535  restopn2  14851  txcn  14943  txlm  14947  isxms2  15120  rpcxpmul2  15581  gausslemma2dlem0i  15730  incistruhgr  15884  upgredg2vtx  15940  upgredgpr  15941  uhgr2edg  15998  bj-om  16258  bj-inf2vnlem2  16292  bj-inf2vn  16295  bj-inf2vn2  16296  dom1o  16314