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  697  limelon  4400  eldifpw  4478  ssonuni  4488  onsucuni2  4564  peano2  4595  limom  4614  elrnmpt1  4879  cnveqb  5085  cnveq0  5086  relcoi1  5161  ndmfvg  5547  ffvresb  5680  caovord3d  6045  poxp  6233  nnm0r  6480  nnacl  6481  nnacom  6485  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  nnmcom  6490  brecop  6625  ecopovtrn  6632  ecopovtrng  6635  elpm2r  6666  map0g  6688  fundmen  6806  mapxpen  6848  phpm  6865  f1vrnfibi  6944  elfir  6972  mulcmpblnq  7367  ordpipqqs  7373  mulcmpblnq0  7443  genpprecll  7513  genppreclu  7514  addcmpblnr  7738  ax1rid  7876  axpre-mulgt0  7886  cnegexlem1  8132  msqge0  8573  mulge0  8576  ltleap  8589  nnmulcl  8940  nnsub  8958  elnn0z  9266  ztri3or0  9295  nneoor  9355  uz11  9550  xltnegi  9835  frec2uzuzd  10402  seq3fveq2  10469  seq3shft2  10473  seq3split  10479  seq3caopr3  10481  seq3id2  10509  seq3homo  10510  m1expcl2  10542  expadd  10562  expmul  10565  faclbnd  10721  hashfzp1  10804  hashfacen  10816  seq3coll  10822  caucvgrelemcau  10989  recan  11118  rexanre  11229  fsumiun  11485  efexp  11690  dvdstr  11835  alzdvds  11860  zob  11896  gcdmultiplez  12022  dvdssq  12032  cncongr2  12104  prmdiveq  12236  pythagtriplem2  12266  pcexp  12309  elrestr  12696  ptex  12713  xpsff1o  12768  dfgrp3me  12970  mulgneg2  13017  mulgnnass  13018  mhmmulg  13024  ringadd2  13210  mulgass2  13235  subrgpropd  13369  lmodprop2d  13438  cnfldmulg  13473  cnfldexp  13474  restopn2  13686  txcn  13778  txlm  13782  isxms2  13955  bj-om  14692  bj-inf2vnlem2  14726  bj-inf2vn  14729  bj-inf2vn2  14730