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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibrcom  157  biimprd  158  nbn2  709  anifpdc  999  limelon  4544  eldifpw  4623  ssonuni  4635  onsucuni2  4711  peano2  4742  limom  4761  elrnmpt1  5033  cnveqb  5243  cnveq0  5244  relcoi1  5319  f1ssf1  5671  ndmfvg  5726  ffvresb  5871  caovord3d  6260  poxp  6468  nnm0r  6752  nnacl  6753  nnacom  6757  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  nnmcom  6762  brecop  6899  ecopovtrn  6906  ecopovtrng  6909  elpm2r  6940  map0g  6969  fundmen  7094  dom1o  7116  mapxpen  7148  mapunen  7151  phpm  7167  f1vrnfibi  7259  elfir  7307  mulcmpblnq  7735  ordpipqqs  7741  mulcmpblnq0  7811  genpprecll  7881  genppreclu  7882  addcmpblnr  8106  ax1rid  8244  axpre-mulgt0  8254  cnegexlem1  8501  msqge0  8944  mulge0  8947  ltleap  8960  nnmulcl  9325  nnsub  9343  elnn0z  9657  ztri3or0  9686  nneoor  9748  uz11  9945  xltnegi  10237  frec2uzuzd  10839  seq3fveq2  10912  seqfveq2g  10914  seq3shft2  10918  seqshft2g  10919  seq3split  10925  seqsplitg  10926  seq3caopr3  10928  seqcaopr3g  10929  seqf1oglem2a  10955  seq3id2  10963  seq3homo  10964  seqhomog  10967  m1expcl2  10998  expadd  11018  expmul  11021  faclbnd  11179  hashfzp1  11265  hashmap  11268  hashfacen  11284  hashf1lem2  11286  hashf1  11287  seq3coll  11294  wrdsymb0  11337  len0nnbi  11339  wrd2ind  11495  pfxccatin12lem2c  11502  pfxccatin12lem2  11503  swrdccatin1d  11515  caucvgrelemcau  11746  recan  11875  rexanre  11986  fsumiun  12244  efexp  12449  dvdstr  12595  alzdvds  12621  zob  12658  bitsinv1  12729  gcdmultiplez  12798  dvdssq  12808  cncongr2  12882  prmdiveq  13014  pythagtriplem2  13045  pcexp  13088  elrestr  13601  ptex  13618  xpsff1o  13670  dfgrp3me  13905  mulgneg2  13959  mulgnnass  13960  mhmmulg  13966  rngpropd  14254  ringadd2  14332  mulgass2  14363  opprrngbg  14383  opprsubrngg  14519  subrngpropd  14524  subrgpropd  14561  rhmpropd  14562  lmodprop2d  14685  cnfldmulg  14913  cnfldexp  14914  assapropd  15014  restopn2  15284  txcn  15376  txlm  15380  isxms2  15553  rpcxpmul2  16015  gausslemma2dlem0i  16176  incistruhgr  16331  upgredg2vtx  16389  upgredgpr  16390  uhgr2edg  16447  wlkres  16620  clwwlknonex2  16680  eupth2lem3lem6fi  16712  bj-om  16963  bj-inf2vnlem2  16997  bj-inf2vn  17000  bj-inf2vn2  17001