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  4525  eldifpw  4603  ssonuni  4615  onsucuni2  4691  peano2  4722  limom  4741  elrnmpt1  5013  cnveqb  5223  cnveq0  5224  relcoi1  5299  f1ssf1  5651  ndmfvg  5706  ffvresb  5845  caovord3d  6233  poxp  6441  nnm0r  6725  nnacl  6726  nnacom  6730  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  nnmcom  6735  brecop  6872  ecopovtrn  6879  ecopovtrng  6882  elpm2r  6913  map0g  6935  fundmen  7060  dom1o  7082  mapxpen  7114  mapunen  7117  phpm  7133  f1vrnfibi  7225  elfir  7273  mulcmpblnq  7699  ordpipqqs  7705  mulcmpblnq0  7775  genpprecll  7845  genppreclu  7846  addcmpblnr  8070  ax1rid  8208  axpre-mulgt0  8218  cnegexlem1  8464  msqge0  8907  mulge0  8910  ltleap  8923  nnmulcl  9275  nnsub  9293  elnn0z  9607  ztri3or0  9636  nneoor  9698  uz11  9895  xltnegi  10187  frec2uzuzd  10788  seq3fveq2  10861  seqfveq2g  10863  seq3shft2  10867  seqshft2g  10868  seq3split  10874  seqsplitg  10875  seq3caopr3  10877  seqcaopr3g  10878  seqf1oglem2a  10904  seq3id2  10912  seq3homo  10913  seqhomog  10916  m1expcl2  10947  expadd  10967  expmul  10970  faclbnd  11128  hashfzp1  11214  hashmap  11217  hashfacen  11233  seq3coll  11239  wrdsymb0  11282  len0nnbi  11284  wrd2ind  11440  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  swrdccatin1d  11460  caucvgrelemcau  11690  recan  11819  rexanre  11930  fsumiun  12188  efexp  12393  dvdstr  12539  alzdvds  12565  zob  12602  bitsinv1  12673  gcdmultiplez  12742  dvdssq  12752  cncongr2  12826  prmdiveq  12958  pythagtriplem2  12989  pcexp  13032  elrestr  13544  ptex  13561  xpsff1o  13613  dfgrp3me  13855  mulgneg2  13909  mulgnnass  13910  mhmmulg  13916  rngpropd  14194  ringadd2  14270  mulgass2  14301  opprrngbg  14321  opprsubrngg  14457  subrngpropd  14462  subrgpropd  14499  rhmpropd  14500  lmodprop2d  14622  cnfldmulg  14850  cnfldexp  14851  restopn2  15174  txcn  15266  txlm  15270  isxms2  15443  rpcxpmul2  15904  gausslemma2dlem0i  16056  incistruhgr  16211  upgredg2vtx  16269  upgredgpr  16270  uhgr2edg  16327  wlkres  16500  clwwlknonex2  16560  eupth2lem3lem6fi  16592  bj-om  16833  bj-inf2vnlem2  16867  bj-inf2vn  16870  bj-inf2vn2  16871