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  7736  ordpipqqs  7742  mulcmpblnq0  7812  genpprecll  7882  genppreclu  7883  addcmpblnr  8107  ax1rid  8245  axpre-mulgt0  8255  cnegexlem1  8503  msqge0  8947  mulge0  8950  ltleap  8963  nnmulcl  9328  nnsub  9346  elnn0z  9662  ztri3or0  9691  nneoor  9753  uz11  9955  xltnegi  10248  frec2uzuzd  10854  seq3fveq2  10927  seqfveq2g  10929  seq3shft2  10933  seqshft2g  10934  seq3split  10940  seqsplitg  10941  seq3caopr3  10943  seqcaopr3g  10944  seqf1oglem2a  10970  seq3id2  10978  seq3homo  10979  seqhomog  10982  m1expcl2  11013  expadd  11033  expmul  11036  faclbnd  11195  hashfzp1  11281  hashmap  11284  hashfacen  11300  hashf1lem2  11302  hashf1  11303  seq3coll  11310  wrdsymb0  11353  len0nnbi  11355  wrd2ind  11511  pfxccatin12lem2c  11518  pfxccatin12lem2  11519  swrdccatin1d  11531  caucvgrelemcau  11762  recan  11892  rexanre  12003  fsumiun  12263  efexp  12468  dvdstr  12614  alzdvds  12640  zob  12677  bitsinv1  12748  gcdmultiplez  12817  dvdssq  12827  cncongr2  12901  prmdiveq  13037  pythagtriplem2  13068  pcexp  13111  elrestr  13654  ptex  13671  xpsff1o  13723  dfgrp3me  13958  mulgneg2  14012  mulgnnass  14013  mhmmulg  14019  rngpropd  14338  ringadd2  14416  mulgass2  14447  opprrngbg  14467  opprsubrngg  14603  subrngpropd  14608  subrgpropd  14645  rhmpropd  14646  lmodprop2d  14769  cnfldmulg  14997  cnfldexp  14998  assapropd  15098  restopn2  15375  txcn  15467  txlm  15471  isxms2  15644  rpcxpmul2  16110  chtqub  16257  gausslemma2dlem0i  16342  incistruhgr  16497  upgredg2vtx  16555  upgredgpr  16556  uhgr2edg  16613  wlkres  16786  clwwlknonex2  16846  eupth2lem3lem6fi  16878  bj-om  17129  bj-inf2vnlem2  17163  bj-inf2vn  17166  bj-inf2vn2  17167