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  697  limelon  4401  eldifpw  4479  ssonuni  4489  onsucuni2  4565  peano2  4596  limom  4615  elrnmpt1  4880  cnveqb  5086  cnveq0  5087  relcoi1  5162  ndmfvg  5548  ffvresb  5682  caovord3d  6048  poxp  6236  nnm0r  6483  nnacl  6484  nnacom  6488  nnaass  6489  nndi  6490  nnmass  6491  nnmsucr  6492  nnmcom  6493  brecop  6628  ecopovtrn  6635  ecopovtrng  6638  elpm2r  6669  map0g  6691  fundmen  6809  mapxpen  6851  phpm  6868  f1vrnfibi  6947  elfir  6975  mulcmpblnq  7370  ordpipqqs  7376  mulcmpblnq0  7446  genpprecll  7516  genppreclu  7517  addcmpblnr  7741  ax1rid  7879  axpre-mulgt0  7889  cnegexlem1  8135  msqge0  8576  mulge0  8579  ltleap  8592  nnmulcl  8943  nnsub  8961  elnn0z  9269  ztri3or0  9298  nneoor  9358  uz11  9553  xltnegi  9838  frec2uzuzd  10405  seq3fveq2  10472  seq3shft2  10476  seq3split  10482  seq3caopr3  10484  seq3id2  10512  seq3homo  10513  m1expcl2  10545  expadd  10565  expmul  10568  faclbnd  10724  hashfzp1  10807  hashfacen  10819  seq3coll  10825  caucvgrelemcau  10992  recan  11121  rexanre  11232  fsumiun  11488  efexp  11693  dvdstr  11838  alzdvds  11863  zob  11899  gcdmultiplez  12025  dvdssq  12035  cncongr2  12107  prmdiveq  12239  pythagtriplem2  12269  pcexp  12312  elrestr  12702  ptex  12719  xpsff1o  12774  dfgrp3me  12976  mulgneg2  13023  mulgnnass  13024  mhmmulg  13030  ringadd2  13216  mulgass2  13241  subrgpropd  13375  lmodprop2d  13444  cnfldmulg  13610  cnfldexp  13611  restopn2  13823  txcn  13915  txlm  13919  isxms2  14092  bj-om  14829  bj-inf2vnlem2  14863  bj-inf2vn  14866  bj-inf2vn2  14867