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  4490  eldifpw  4568  ssonuni  4580  onsucuni2  4656  peano2  4687  limom  4706  elrnmpt1  4975  cnveqb  5184  cnveq0  5185  relcoi1  5260  ndmfvg  5660  ffvresb  5800  caovord3d  6182  poxp  6384  nnm0r  6633  nnacl  6634  nnacom  6638  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  nnmcom  6643  brecop  6780  ecopovtrn  6787  ecopovtrng  6790  elpm2r  6821  map0g  6843  fundmen  6967  dom1o  6985  mapxpen  7017  phpm  7035  f1vrnfibi  7123  elfir  7151  mulcmpblnq  7566  ordpipqqs  7572  mulcmpblnq0  7642  genpprecll  7712  genppreclu  7713  addcmpblnr  7937  ax1rid  8075  axpre-mulgt0  8085  cnegexlem1  8332  msqge0  8774  mulge0  8777  ltleap  8790  nnmulcl  9142  nnsub  9160  elnn0z  9470  ztri3or0  9499  nneoor  9560  uz11  9757  xltnegi  10043  frec2uzuzd  10636  seq3fveq2  10709  seqfveq2g  10711  seq3shft2  10715  seqshft2g  10716  seq3split  10722  seqsplitg  10723  seq3caopr3  10725  seqcaopr3g  10726  seqf1oglem2a  10752  seq3id2  10760  seq3homo  10761  seqhomog  10764  m1expcl2  10795  expadd  10815  expmul  10818  faclbnd  10975  hashfzp1  11059  hashfacen  11071  seq3coll  11077  wrdsymb0  11117  len0nnbi  11119  wrd2ind  11270  pfxccatin12lem2c  11277  pfxccatin12lem2  11278  swrdccatin1d  11290  caucvgrelemcau  11506  recan  11635  rexanre  11746  fsumiun  12003  efexp  12208  dvdstr  12354  alzdvds  12380  zob  12417  bitsinv1  12488  gcdmultiplez  12557  dvdssq  12567  cncongr2  12641  prmdiveq  12773  pythagtriplem2  12804  pcexp  12847  elrestr  13295  ptex  13312  xpsff1o  13397  dfgrp3me  13648  mulgneg2  13708  mulgnnass  13709  mhmmulg  13715  rngpropd  13933  ringadd2  14005  mulgass2  14036  opprrngbg  14056  opprsubrngg  14190  subrngpropd  14195  subrgpropd  14232  rhmpropd  14233  lmodprop2d  14327  cnfldmulg  14555  cnfldexp  14556  restopn2  14872  txcn  14964  txlm  14968  isxms2  15141  rpcxpmul2  15602  gausslemma2dlem0i  15751  incistruhgr  15905  upgredg2vtx  15961  upgredgpr  15962  uhgr2edg  16019  wlkres  16118  bj-om  16355  bj-inf2vnlem2  16389  bj-inf2vn  16392  bj-inf2vn2  16393