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  698  limelon  4445  eldifpw  4523  ssonuni  4535  onsucuni2  4611  peano2  4642  limom  4661  elrnmpt1  4928  cnveqb  5137  cnveq0  5138  relcoi1  5213  ndmfvg  5606  ffvresb  5742  caovord3d  6116  poxp  6317  nnm0r  6564  nnacl  6565  nnacom  6569  nnaass  6570  nndi  6571  nnmass  6572  nnmsucr  6573  nnmcom  6574  brecop  6711  ecopovtrn  6718  ecopovtrng  6721  elpm2r  6752  map0g  6774  fundmen  6897  mapxpen  6944  phpm  6961  f1vrnfibi  7046  elfir  7074  mulcmpblnq  7480  ordpipqqs  7486  mulcmpblnq0  7556  genpprecll  7626  genppreclu  7627  addcmpblnr  7851  ax1rid  7989  axpre-mulgt0  7999  cnegexlem1  8246  msqge0  8688  mulge0  8691  ltleap  8704  nnmulcl  9056  nnsub  9074  elnn0z  9384  ztri3or0  9413  nneoor  9474  uz11  9670  xltnegi  9956  frec2uzuzd  10545  seq3fveq2  10618  seqfveq2g  10620  seq3shft2  10624  seqshft2g  10625  seq3split  10631  seqsplitg  10632  seq3caopr3  10634  seqcaopr3g  10635  seqf1oglem2a  10661  seq3id2  10669  seq3homo  10670  seqhomog  10673  m1expcl2  10704  expadd  10724  expmul  10727  faclbnd  10884  hashfzp1  10967  hashfacen  10979  seq3coll  10985  wrdsymb0  11024  len0nnbi  11026  caucvgrelemcau  11262  recan  11391  rexanre  11502  fsumiun  11759  efexp  11964  dvdstr  12110  alzdvds  12136  zob  12173  bitsinv1  12244  gcdmultiplez  12313  dvdssq  12323  cncongr2  12397  prmdiveq  12529  pythagtriplem2  12560  pcexp  12603  elrestr  13050  ptex  13067  xpsff1o  13152  dfgrp3me  13403  mulgneg2  13463  mulgnnass  13464  mhmmulg  13470  rngpropd  13688  ringadd2  13760  mulgass2  13791  opprrngbg  13811  opprsubrngg  13944  subrngpropd  13949  subrgpropd  13986  rhmpropd  13987  lmodprop2d  14081  cnfldmulg  14309  cnfldexp  14310  restopn2  14626  txcn  14718  txlm  14722  isxms2  14895  rpcxpmul2  15356  gausslemma2dlem0i  15505  bj-om  15835  bj-inf2vnlem2  15869  bj-inf2vn  15872  bj-inf2vn2  15873