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  704  anifpdc  994  limelon  4496  eldifpw  4574  ssonuni  4586  onsucuni2  4662  peano2  4693  limom  4712  elrnmpt1  4983  cnveqb  5192  cnveq0  5193  relcoi1  5268  f1ssf1  5615  ndmfvg  5670  ffvresb  5810  caovord3d  6193  poxp  6397  nnm0r  6647  nnacl  6648  nnacom  6652  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  nnmcom  6657  brecop  6794  ecopovtrn  6801  ecopovtrng  6804  elpm2r  6835  map0g  6857  fundmen  6981  dom1o  7002  mapxpen  7034  phpm  7052  f1vrnfibi  7144  elfir  7172  mulcmpblnq  7588  ordpipqqs  7594  mulcmpblnq0  7664  genpprecll  7734  genppreclu  7735  addcmpblnr  7959  ax1rid  8097  axpre-mulgt0  8107  cnegexlem1  8354  msqge0  8796  mulge0  8799  ltleap  8812  nnmulcl  9164  nnsub  9182  elnn0z  9492  ztri3or0  9521  nneoor  9582  uz11  9779  xltnegi  10070  frec2uzuzd  10665  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seqf1oglem2a  10781  seq3id2  10789  seq3homo  10790  seqhomog  10793  m1expcl2  10824  expadd  10844  expmul  10847  faclbnd  11004  hashfzp1  11089  hashfacen  11101  seq3coll  11107  wrdsymb0  11150  len0nnbi  11152  wrd2ind  11308  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  swrdccatin1d  11328  caucvgrelemcau  11558  recan  11687  rexanre  11798  fsumiun  12056  efexp  12261  dvdstr  12407  alzdvds  12433  zob  12470  bitsinv1  12541  gcdmultiplez  12610  dvdssq  12620  cncongr2  12694  prmdiveq  12826  pythagtriplem2  12857  pcexp  12900  elrestr  13348  ptex  13365  xpsff1o  13450  dfgrp3me  13701  mulgneg2  13761  mulgnnass  13762  mhmmulg  13768  rngpropd  13987  ringadd2  14059  mulgass2  14090  opprrngbg  14110  opprsubrngg  14244  subrngpropd  14249  subrgpropd  14286  rhmpropd  14287  lmodprop2d  14381  cnfldmulg  14609  cnfldexp  14610  restopn2  14926  txcn  15018  txlm  15022  isxms2  15195  rpcxpmul2  15656  gausslemma2dlem0i  15805  incistruhgr  15960  upgredg2vtx  16018  upgredgpr  16019  uhgr2edg  16076  wlkres  16249  clwwlknonex2  16309  eupth2lem3lem6fi  16341  bj-om  16583  bj-inf2vnlem2  16617  bj-inf2vn  16620  bj-inf2vn2  16621