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  4435  eldifpw  4513  ssonuni  4525  onsucuni2  4601  peano2  4632  limom  4651  elrnmpt1  4918  cnveqb  5126  cnveq0  5127  relcoi1  5202  ndmfvg  5592  ffvresb  5728  caovord3d  6098  poxp  6299  nnm0r  6546  nnacl  6547  nnacom  6551  nnaass  6552  nndi  6553  nnmass  6554  nnmsucr  6555  nnmcom  6556  brecop  6693  ecopovtrn  6700  ecopovtrng  6703  elpm2r  6734  map0g  6756  fundmen  6874  mapxpen  6918  phpm  6935  f1vrnfibi  7020  elfir  7048  mulcmpblnq  7452  ordpipqqs  7458  mulcmpblnq0  7528  genpprecll  7598  genppreclu  7599  addcmpblnr  7823  ax1rid  7961  axpre-mulgt0  7971  cnegexlem1  8218  msqge0  8660  mulge0  8663  ltleap  8676  nnmulcl  9028  nnsub  9046  elnn0z  9356  ztri3or0  9385  nneoor  9445  uz11  9641  xltnegi  9927  frec2uzuzd  10511  seq3fveq2  10584  seqfveq2g  10586  seq3shft2  10590  seqshft2g  10591  seq3split  10597  seqsplitg  10598  seq3caopr3  10600  seqcaopr3g  10601  seqf1oglem2a  10627  seq3id2  10635  seq3homo  10636  seqhomog  10639  m1expcl2  10670  expadd  10690  expmul  10693  faclbnd  10850  hashfzp1  10933  hashfacen  10945  seq3coll  10951  wrdsymb0  10984  len0nnbi  10986  caucvgrelemcau  11162  recan  11291  rexanre  11402  fsumiun  11659  efexp  11864  dvdstr  12010  alzdvds  12036  zob  12073  bitsinv1  12144  gcdmultiplez  12213  dvdssq  12223  cncongr2  12297  prmdiveq  12429  pythagtriplem2  12460  pcexp  12503  elrestr  12949  ptex  12966  xpsff1o  13051  dfgrp3me  13302  mulgneg2  13362  mulgnnass  13363  mhmmulg  13369  rngpropd  13587  ringadd2  13659  mulgass2  13690  opprrngbg  13710  opprsubrngg  13843  subrngpropd  13848  subrgpropd  13885  rhmpropd  13886  lmodprop2d  13980  cnfldmulg  14208  cnfldexp  14209  restopn2  14503  txcn  14595  txlm  14599  isxms2  14772  rpcxpmul2  15233  gausslemma2dlem0i  15382  bj-om  15667  bj-inf2vnlem2  15701  bj-inf2vn  15704  bj-inf2vn2  15705