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  11271  pfxccatin12lem2c  11278  pfxccatin12lem2  11279  swrdccatin1d  11291  caucvgrelemcau  11507  recan  11636  rexanre  11747  fsumiun  12004  efexp  12209  dvdstr  12355  alzdvds  12381  zob  12418  bitsinv1  12489  gcdmultiplez  12558  dvdssq  12568  cncongr2  12642  prmdiveq  12774  pythagtriplem2  12805  pcexp  12848  elrestr  13296  ptex  13313  xpsff1o  13398  dfgrp3me  13649  mulgneg2  13709  mulgnnass  13710  mhmmulg  13716  rngpropd  13934  ringadd2  14006  mulgass2  14037  opprrngbg  14057  opprsubrngg  14191  subrngpropd  14196  subrgpropd  14233  rhmpropd  14234  lmodprop2d  14328  cnfldmulg  14556  cnfldexp  14557  restopn2  14873  txcn  14965  txlm  14969  isxms2  15142  rpcxpmul2  15603  gausslemma2dlem0i  15752  incistruhgr  15906  upgredg2vtx  15962  upgredgpr  15963  uhgr2edg  16020  wlkres  16123  bj-om  16383  bj-inf2vnlem2  16417  bj-inf2vn  16420  bj-inf2vn2  16421