Theorem biimtrrid 153

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
biimtrrid.1	|- ( ps <-> ph )
biimtrrid.2	|- ( ch -> ( ps -> th ) )

Assertion

Ref	Expression
biimtrrid	|- ( ch -> ( ph -> th ) )

Proof of Theorem biimtrrid

Step	Hyp	Ref	Expression
1		biimtrrid.1	. . 3 |- ( ps <-> ph )
2	1	biimpri 133	. 2 |- ( ph -> ps )
3		biimtrrid.2	. 2 |- ( ch -> ( ps -> th ) )
4	2, 3	syl5 32	1 |- ( ch -> ( ph -> th ) )

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:  3imtr3g  204  19.37-1  1722  mo3h  2136  necon1bidc  2466  necon4aidc  2482  r19.30dc  2692  ceqex  2947  ssdisj  3569  ralidm  3614  exmid1dc  4318  rexxfrd  4589  sucprcreg  4676  imain  5443  f0rn0  5567  funopfv  5719  mpteqb  5773  funfvima  5923  fliftfun  5975  fvdifsuppst  6457  suppssrst  6474  suppssrgst  6475  iinerm  6854  eroveu  6873  th3qlem1  6884  updjudhf  7383  elni2  7645  genpdisj  7854  lttri3  8369  seqf1og  10907  nn0ltexp2  11096  zfz1iso  11238  ccatalpha  11326  cau3lem  11824  maxleast  11923  rexanre  11930  climcau  12057  summodc  12094  mertenslem2  12247  prodmodclem2  12288  prodmodc  12289  fprodseq  12294  bitsfzolem  12665  bitsfzo  12666  divgcdcoprmex  12824  prmind2  12842  pcqmul  13026  pcxcl  13034  pcadd  13063  mul4sq  13117  issubg2m  13942  dvdsrtr  14346  unitgrp  14361  subrgintm  14489  islssm  14631  znidom  14931  opnneiid  15155  txuni2  15247  txbas  15249  txbasval  15258  txlm  15270  blin2  15423  tgqioo  15546  plyadd  15742  plymul  15743  lgsquad2lem2  16081  2sqlem5  16118  uhgr2edg  16327  uspgr2wlkeq  16486  bj-charfunr  16706