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  4520  eldifpw  4598  ssonuni  4610  onsucuni2  4686  peano2  4717  limom  4736  elrnmpt1  5008  cnveqb  5218  cnveq0  5219  relcoi1  5294  f1ssf1  5646  ndmfvg  5701  ffvresb  5840  caovord3d  6225  poxp  6428  nnm0r  6712  nnacl  6713  nnacom  6717  nnaass  6718  nndi  6719  nnmass  6720  nnmsucr  6721  nnmcom  6722  brecop  6859  ecopovtrn  6866  ecopovtrng  6869  elpm2r  6900  map0g  6922  fundmen  7047  dom1o  7069  mapxpen  7101  mapunen  7104  phpm  7120  f1vrnfibi  7212  elfir  7260  mulcmpblnq  7683  ordpipqqs  7689  mulcmpblnq0  7759  genpprecll  7829  genppreclu  7830  addcmpblnr  8054  ax1rid  8192  axpre-mulgt0  8202  cnegexlem1  8448  msqge0  8890  mulge0  8893  ltleap  8906  nnmulcl  9258  nnsub  9276  elnn0z  9590  ztri3or0  9619  nneoor  9680  uz11  9877  xltnegi  10168  frec2uzuzd  10764  seq3fveq2  10837  seqfveq2g  10839  seq3shft2  10843  seqshft2g  10844  seq3split  10850  seqsplitg  10851  seq3caopr3  10853  seqcaopr3g  10854  seqf1oglem2a  10880  seq3id2  10888  seq3homo  10889  seqhomog  10892  m1expcl2  10923  expadd  10943  expmul  10946  faclbnd  11103  hashfzp1  11189  hashmap  11192  hashfacen  11208  seq3coll  11214  wrdsymb0  11257  len0nnbi  11259  wrd2ind  11415  pfxccatin12lem2c  11422  pfxccatin12lem2  11423  swrdccatin1d  11435  caucvgrelemcau  11665  recan  11794  rexanre  11905  fsumiun  12163  efexp  12368  dvdstr  12514  alzdvds  12540  zob  12577  bitsinv1  12648  gcdmultiplez  12717  dvdssq  12727  cncongr2  12801  prmdiveq  12933  pythagtriplem2  12964  pcexp  13007  elrestr  13460  ptex  13477  xpsff1o  13562  dfgrp3me  13813  mulgneg2  13873  mulgnnass  13874  mhmmulg  13880  rngpropd  14099  ringadd2  14171  mulgass2  14202  opprrngbg  14222  opprsubrngg  14356  subrngpropd  14361  subrgpropd  14398  rhmpropd  14399  lmodprop2d  14496  cnfldmulg  14724  cnfldexp  14725  restopn2  15048  txcn  15140  txlm  15144  isxms2  15317  rpcxpmul2  15778  gausslemma2dlem0i  15930  incistruhgr  16085  upgredg2vtx  16143  upgredgpr  16144  uhgr2edg  16201  wlkres  16374  clwwlknonex2  16434  eupth2lem3lem6fi  16466  bj-om  16707  bj-inf2vnlem2  16741  bj-inf2vn  16744  bj-inf2vn2  16745