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  6756  nnacl  6757  nnacom  6761  nnaass  6762  nndi  6763  nnmass  6764  nnmsucr  6765  nnmcom  6766  brecop  6903  ecopovtrn  6910  ecopovtrng  6913  elpm2r  6944  map0g  6973  fundmen  7098  dom1o  7120  mapxpen  7152  mapunen  7155  phpm  7171  f1vrnfibi  7263  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  9668  ztri3or0  9697  nneoor  9759  uz11  9961  xltnegi  10254  frec2uzuzd  10860  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seqf1oglem2a  10976  seq3id2  10984  seq3homo  10985  seqhomog  10988  m1expcl2  11019  expadd  11039  expmul  11042  faclbnd  11201  hashfzp1  11287  hashmap  11290  hashfacen  11306  hashf1lem2  11308  hashf1  11309  seq3coll  11316  wrdsymb0  11359  len0nnbi  11361  wrd2ind  11517  pfxccatin12lem2c  11524  pfxccatin12lem2  11525  swrdccatin1d  11537  caucvgrelemcau  11768  recan  11898  rexanre  12009  fsumiun  12269  efexp  12474  dvdstr  12620  alzdvds  12646  zob  12683  bitsinv1  12754  gcdmultiplez  12823  dvdssq  12833  cncongr2  12907  prmdiveq  13043  pythagtriplem2  13074  pcexp  13117  elrestr  13660  ptex  13677  xpsff1o  13729  dfgrp3me  13964  mulgneg2  14018  mulgnnass  14019  mhmmulg  14025  gsum2dfilem2  14272  rngpropd  14361  ringadd2  14439  mulgass2  14470  opprrngbg  14492  opprsubrngg  14628  subrngpropd  14633  subrgpropd  14670  rhmpropd  14671  lmodprop2d  14794  cnfldmulg  15022  cnfldexp  15023  assapropd  15123  restopn2  15409  txcn  15501  txlm  15505  isxms2  15678  rpcxpmul2  16146  chtqub  16296  gausslemma2dlem0i  16381  incistruhgr  16536  upgredg2vtx  16594  upgredgpr  16595  uhgr2edg  16652  wlkres  16825  clwwlknonex2  16885  eupth2lem3lem6fi  16917  bj-om  17168  bj-inf2vnlem2  17202  bj-inf2vn  17205  bj-inf2vn2  17206