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  8502  msqge0  8946  mulge0  8949  ltleap  8962  nnmulcl  9327  nnsub  9345  elnn0z  9661  ztri3or0  9690  nneoor  9752  uz11  9954  xltnegi  10247  frec2uzuzd  10852  seq3fveq2  10925  seqfveq2g  10927  seq3shft2  10931  seqshft2g  10932  seq3split  10938  seqsplitg  10939  seq3caopr3  10941  seqcaopr3g  10942  seqf1oglem2a  10968  seq3id2  10976  seq3homo  10977  seqhomog  10980  m1expcl2  11011  expadd  11031  expmul  11034  faclbnd  11193  hashfzp1  11279  hashmap  11282  hashfacen  11298  hashf1lem2  11300  hashf1  11301  seq3coll  11308  wrdsymb0  11351  len0nnbi  11353  wrd2ind  11509  pfxccatin12lem2c  11516  pfxccatin12lem2  11517  swrdccatin1d  11529  caucvgrelemcau  11760  recan  11890  rexanre  12001  fsumiun  12260  efexp  12465  dvdstr  12611  alzdvds  12637  zob  12674  bitsinv1  12745  gcdmultiplez  12814  dvdssq  12824  cncongr2  12898  prmdiveq  13034  pythagtriplem2  13065  pcexp  13108  elrestr  13650  ptex  13667  xpsff1o  13719  dfgrp3me  13954  mulgneg2  14008  mulgnnass  14009  mhmmulg  14015  rngpropd  14303  ringadd2  14381  mulgass2  14412  opprrngbg  14432  opprsubrngg  14568  subrngpropd  14573  subrgpropd  14610  rhmpropd  14611  lmodprop2d  14734  cnfldmulg  14962  cnfldexp  14963  assapropd  15063  restopn2  15333  txcn  15425  txlm  15429  isxms2  15602  rpcxpmul2  16068  gausslemma2dlem0i  16274  incistruhgr  16429  upgredg2vtx  16487  upgredgpr  16488  uhgr2edg  16545  wlkres  16718  clwwlknonex2  16778  eupth2lem3lem6fi  16810  bj-om  17061  bj-inf2vnlem2  17095  bj-inf2vn  17098  bj-inf2vn2  17099