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  709  anifpdc  999  limelon  4539  eldifpw  4618  ssonuni  4630  onsucuni2  4706  peano2  4737  limom  4756  elrnmpt1  5028  cnveqb  5238  cnveq0  5239  relcoi1  5314  f1ssf1  5666  ndmfvg  5721  ffvresb  5862  caovord3d  6250  poxp  6458  nnm0r  6742  nnacl  6743  nnacom  6747  nnaass  6748  nndi  6749  nnmass  6750  nnmsucr  6751  nnmcom  6752  brecop  6889  ecopovtrn  6896  ecopovtrng  6899  elpm2r  6930  map0g  6959  fundmen  7084  dom1o  7106  mapxpen  7138  mapunen  7141  phpm  7157  f1vrnfibi  7249  elfir  7297  mulcmpblnq  7725  ordpipqqs  7731  mulcmpblnq0  7801  genpprecll  7871  genppreclu  7872  addcmpblnr  8096  ax1rid  8234  axpre-mulgt0  8244  cnegexlem1  8491  msqge0  8934  mulge0  8937  ltleap  8950  nnmulcl  9304  nnsub  9322  elnn0z  9636  ztri3or0  9665  nneoor  9727  uz11  9924  xltnegi  10216  frec2uzuzd  10817  seq3fveq2  10890  seqfveq2g  10892  seq3shft2  10896  seqshft2g  10897  seq3split  10903  seqsplitg  10904  seq3caopr3  10906  seqcaopr3g  10907  seqf1oglem2a  10933  seq3id2  10941  seq3homo  10942  seqhomog  10945  m1expcl2  10976  expadd  10996  expmul  10999  faclbnd  11157  hashfzp1  11243  hashmap  11246  hashfacen  11262  hashf1lem2  11264  hashf1  11265  seq3coll  11272  wrdsymb0  11315  len0nnbi  11317  wrd2ind  11473  pfxccatin12lem2c  11480  pfxccatin12lem2  11481  swrdccatin1d  11493  caucvgrelemcau  11724  recan  11853  rexanre  11964  fsumiun  12222  efexp  12427  dvdstr  12573  alzdvds  12599  zob  12636  bitsinv1  12707  gcdmultiplez  12776  dvdssq  12786  cncongr2  12860  prmdiveq  12992  pythagtriplem2  13023  pcexp  13066  elrestr  13578  ptex  13595  xpsff1o  13647  dfgrp3me  13882  mulgneg2  13936  mulgnnass  13937  mhmmulg  13943  rngpropd  14229  ringadd2  14305  mulgass2  14336  opprrngbg  14356  opprsubrngg  14492  subrngpropd  14497  subrgpropd  14534  rhmpropd  14535  lmodprop2d  14657  cnfldmulg  14885  cnfldexp  14886  restopn2  15207  txcn  15299  txlm  15303  isxms2  15476  rpcxpmul2  15938  gausslemma2dlem0i  16090  incistruhgr  16245  upgredg2vtx  16303  upgredgpr  16304  uhgr2edg  16361  wlkres  16534  clwwlknonex2  16594  eupth2lem3lem6fi  16626  bj-om  16877  bj-inf2vnlem2  16911  bj-inf2vn  16914  bj-inf2vn2  16915