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  702  anifpdc  992  limelon  4494  eldifpw  4572  ssonuni  4584  onsucuni2  4660  peano2  4691  limom  4710  elrnmpt1  4981  cnveqb  5190  cnveq0  5191  relcoi1  5266  ndmfvg  5666  ffvresb  5806  caovord3d  6188  poxp  6392  nnm0r  6642  nnacl  6643  nnacom  6647  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  nnmcom  6652  brecop  6789  ecopovtrn  6796  ecopovtrng  6799  elpm2r  6830  map0g  6852  fundmen  6976  dom1o  6997  mapxpen  7029  phpm  7047  f1vrnfibi  7135  elfir  7163  mulcmpblnq  7578  ordpipqqs  7584  mulcmpblnq0  7654  genpprecll  7724  genppreclu  7725  addcmpblnr  7949  ax1rid  8087  axpre-mulgt0  8097  cnegexlem1  8344  msqge0  8786  mulge0  8789  ltleap  8802  nnmulcl  9154  nnsub  9172  elnn0z  9482  ztri3or0  9511  nneoor  9572  uz11  9769  xltnegi  10060  frec2uzuzd  10654  seq3fveq2  10727  seqfveq2g  10729  seq3shft2  10733  seqshft2g  10734  seq3split  10740  seqsplitg  10741  seq3caopr3  10743  seqcaopr3g  10744  seqf1oglem2a  10770  seq3id2  10778  seq3homo  10779  seqhomog  10782  m1expcl2  10813  expadd  10833  expmul  10836  faclbnd  10993  hashfzp1  11078  hashfacen  11090  seq3coll  11096  wrdsymb0  11136  len0nnbi  11138  wrd2ind  11294  pfxccatin12lem2c  11301  pfxccatin12lem2  11302  swrdccatin1d  11314  caucvgrelemcau  11531  recan  11660  rexanre  11771  fsumiun  12028  efexp  12233  dvdstr  12379  alzdvds  12405  zob  12442  bitsinv1  12513  gcdmultiplez  12582  dvdssq  12592  cncongr2  12666  prmdiveq  12798  pythagtriplem2  12829  pcexp  12872  elrestr  13320  ptex  13337  xpsff1o  13422  dfgrp3me  13673  mulgneg2  13733  mulgnnass  13734  mhmmulg  13740  rngpropd  13958  ringadd2  14030  mulgass2  14061  opprrngbg  14081  opprsubrngg  14215  subrngpropd  14220  subrgpropd  14257  rhmpropd  14258  lmodprop2d  14352  cnfldmulg  14580  cnfldexp  14581  restopn2  14897  txcn  14989  txlm  14993  isxms2  15166  rpcxpmul2  15627  gausslemma2dlem0i  15776  incistruhgr  15931  upgredg2vtx  15987  upgredgpr  15988  uhgr2edg  16045  wlkres  16174  clwwlknonex2  16234  bj-om  16468  bj-inf2vnlem2  16502  bj-inf2vn  16505  bj-inf2vn2  16506