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  705  anifpdc  995  limelon  4502  eldifpw  4580  ssonuni  4592  onsucuni2  4668  peano2  4699  limom  4718  elrnmpt1  4989  cnveqb  5199  cnveq0  5200  relcoi1  5275  f1ssf1  5624  ndmfvg  5679  ffvresb  5818  caovord3d  6203  poxp  6406  nnm0r  6690  nnacl  6691  nnacom  6695  nnaass  6696  nndi  6697  nnmass  6698  nnmsucr  6699  nnmcom  6700  brecop  6837  ecopovtrn  6844  ecopovtrng  6847  elpm2r  6878  map0g  6900  fundmen  7024  dom1o  7045  mapxpen  7077  phpm  7095  f1vrnfibi  7187  elfir  7215  mulcmpblnq  7631  ordpipqqs  7637  mulcmpblnq0  7707  genpprecll  7777  genppreclu  7778  addcmpblnr  8002  ax1rid  8140  axpre-mulgt0  8150  cnegexlem1  8396  msqge0  8838  mulge0  8841  ltleap  8854  nnmulcl  9206  nnsub  9224  elnn0z  9536  ztri3or0  9565  nneoor  9626  uz11  9823  xltnegi  10114  frec2uzuzd  10710  seq3fveq2  10783  seqfveq2g  10785  seq3shft2  10789  seqshft2g  10790  seq3split  10796  seqsplitg  10797  seq3caopr3  10799  seqcaopr3g  10800  seqf1oglem2a  10826  seq3id2  10834  seq3homo  10835  seqhomog  10838  m1expcl2  10869  expadd  10889  expmul  10892  faclbnd  11049  hashfzp1  11134  hashfacen  11146  seq3coll  11152  wrdsymb0  11195  len0nnbi  11197  wrd2ind  11353  pfxccatin12lem2c  11360  pfxccatin12lem2  11361  swrdccatin1d  11373  caucvgrelemcau  11603  recan  11732  rexanre  11843  fsumiun  12101  efexp  12306  dvdstr  12452  alzdvds  12478  zob  12515  bitsinv1  12586  gcdmultiplez  12655  dvdssq  12665  cncongr2  12739  prmdiveq  12871  pythagtriplem2  12902  pcexp  12945  elrestr  13393  ptex  13410  xpsff1o  13495  dfgrp3me  13746  mulgneg2  13806  mulgnnass  13807  mhmmulg  13813  rngpropd  14032  ringadd2  14104  mulgass2  14135  opprrngbg  14155  opprsubrngg  14289  subrngpropd  14294  subrgpropd  14331  rhmpropd  14332  lmodprop2d  14427  cnfldmulg  14655  cnfldexp  14656  restopn2  14977  txcn  15069  txlm  15073  isxms2  15246  rpcxpmul2  15707  gausslemma2dlem0i  15859  incistruhgr  16014  upgredg2vtx  16072  upgredgpr  16073  uhgr2edg  16130  wlkres  16303  clwwlknonex2  16363  eupth2lem3lem6fi  16395  bj-om  16636  bj-inf2vnlem2  16670  bj-inf2vn  16673  bj-inf2vn2  16674