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  6192  poxp  6396  nnm0r  6646  nnacl  6647  nnacom  6651  nnaass  6652  nndi  6653  nnmass  6654  nnmsucr  6655  nnmcom  6656  brecop  6793  ecopovtrn  6800  ecopovtrng  6803  elpm2r  6834  map0g  6856  fundmen  6980  dom1o  7001  mapxpen  7033  phpm  7051  f1vrnfibi  7143  elfir  7171  mulcmpblnq  7587  ordpipqqs  7593  mulcmpblnq0  7663  genpprecll  7733  genppreclu  7734  addcmpblnr  7958  ax1rid  8096  axpre-mulgt0  8106  cnegexlem1  8353  msqge0  8795  mulge0  8798  ltleap  8811  nnmulcl  9163  nnsub  9181  elnn0z  9491  ztri3or0  9520  nneoor  9581  uz11  9778  xltnegi  10069  frec2uzuzd  10663  seq3fveq2  10736  seqfveq2g  10738  seq3shft2  10742  seqshft2g  10743  seq3split  10749  seqsplitg  10750  seq3caopr3  10752  seqcaopr3g  10753  seqf1oglem2a  10779  seq3id2  10787  seq3homo  10788  seqhomog  10791  m1expcl2  10822  expadd  10842  expmul  10845  faclbnd  11002  hashfzp1  11087  hashfacen  11099  seq3coll  11105  wrdsymb0  11145  len0nnbi  11147  wrd2ind  11303  pfxccatin12lem2c  11310  pfxccatin12lem2  11311  swrdccatin1d  11323  caucvgrelemcau  11540  recan  11669  rexanre  11780  fsumiun  12037  efexp  12242  dvdstr  12388  alzdvds  12414  zob  12451  bitsinv1  12522  gcdmultiplez  12591  dvdssq  12601  cncongr2  12675  prmdiveq  12807  pythagtriplem2  12838  pcexp  12881  elrestr  13329  ptex  13346  xpsff1o  13431  dfgrp3me  13682  mulgneg2  13742  mulgnnass  13743  mhmmulg  13749  rngpropd  13967  ringadd2  14039  mulgass2  14070  opprrngbg  14090  opprsubrngg  14224  subrngpropd  14229  subrgpropd  14266  rhmpropd  14267  lmodprop2d  14361  cnfldmulg  14589  cnfldexp  14590  restopn2  14906  txcn  14998  txlm  15002  isxms2  15175  rpcxpmul2  15636  gausslemma2dlem0i  15785  incistruhgr  15940  upgredg2vtx  15998  upgredgpr  15999  uhgr2edg  16056  wlkres  16229  clwwlknonex2  16289  bj-om  16532  bj-inf2vnlem2  16566  bj-inf2vn  16569  bj-inf2vn2  16570