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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibrcom  157  biimprd  158  nbn2  709  anifpdc  999  limelon  4546  eldifpw  4625  ssonuni  4637  onsucuni2  4713  peano2  4744  limom  4763  elrnmpt1  5035  cnveqb  5246  cnveq0  5247  relcoi1  5322  f1ssf1  5674  ndmfvg  5729  ffvresb  5874  caovord3d  6263  poxp  6472  nnm0r  6757  nnacl  6758  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  brecop  6904  ecopovtrn  6911  ecopovtrng  6914  elpm2r  6945  map0g  6974  fundmen  7100  dom1o  7122  mapxpen  7154  mapunen  7157  phpm  7173  f1vrnfibi  7265  elfir  7312  mulcmpblnq  7741  ordpipqqs  7747  mulcmpblnq0  7817  genpprecll  7887  genppreclu  7888  addcmpblnr  8112  ax1rid  8250  axpre-mulgt0  8260  cnegexlem1  8508  msqge0  8952  mulge0  8955  ltleap  8968  nnmulcl  9334  nnsub  9352  elnn0z  9666  ztri3or0  9695  nneoor  9758  uz11  9960  xltnegi  10253  frec2uzuzd  10859  seq3fveq2  10932  seqfveq2g  10934  seq3shft2  10938  seqshft2g  10939  seq3split  10945  seqsplitg  10946  seq3caopr3  10948  seqcaopr3g  10949  seqf1oglem2a  10975  seq3id2  10983  seq3homo  10984  seqhomog  10987  m1expcl2  11018  expadd  11038  expmul  11041  faclbnd  11200  hashfzp1  11286  hashmap  11289  hashfacen  11305  hashf1lem2  11307  hashf1  11308  seq3coll  11315  wrdsymb0  11358  len0nnbi  11360  wrd2ind  11516  pfxccatin12lem2c  11523  pfxccatin12lem2  11524  swrdccatin1d  11536  caucvgrelemcau  11767  recan  11897  rexanre  12008  fsumiun  12268  efexp  12473  dvdstr  12619  alzdvds  12645  zob  12682  bitsinv1  12753  gcdmultiplez  12822  dvdssq  12832  cncongr2  12906  prmdiveq  13042  pythagtriplem2  13073  pcexp  13116  elrestr  13659  ptex  13676  xpsff1o  13728  dfgrp3me  13963  mulgneg2  14017  mulgnnass  14018  mhmmulg  14024  gsum2dfilem2  14271  rngpropd  14360  ringadd2  14438  mulgass2  14469  opprrngbg  14491  opprsubrngg  14627  subrngpropd  14632  subrgpropd  14669  rhmpropd  14670  lmodprop2d  14793  cnfldmulg  15021  cnfldexp  15022  assapropd  15122  restopn2  15426  txcn  15518  txlm  15522  isxms2  15695  rpcxpmul2  16163  chtqub  16313  gausslemma2dlem0i  16398  incistruhgr  16553  upgredg2vtx  16611  upgredgpr  16612  uhgr2edg  16669  wlkres  16842  clwwlknonex2  16902  eupth2lem3lem6fi  16934  bj-om  17185  bj-inf2vnlem2  17219  bj-inf2vn  17222  bj-inf2vn2  17223