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  1720  mo3h  2131  necon1bidc  2452  necon4aidc  2468  r19.30dc  2678  ceqex  2930  ssdisj  3548  ralidm  3592  exmid1dc  4284  rexxfrd  4554  sucprcreg  4641  imain  5403  f0rn0  5522  funopfv  5673  mpteqb  5727  funfvima  5875  fliftfun  5926  iinerm  6762  eroveu  6781  th3qlem1  6792  updjudhf  7257  elni2  7512  genpdisj  7721  lttri3  8237  seqf1og  10755  nn0ltexp2  10943  zfz1iso  11076  ccatalpha  11161  cau3lem  11641  maxleast  11740  rexanre  11747  climcau  11874  summodc  11910  mertenslem2  12063  prodmodclem2  12104  prodmodc  12105  fprodseq  12110  bitsfzolem  12481  bitsfzo  12482  divgcdcoprmex  12640  prmind2  12658  pcqmul  12842  pcxcl  12850  pcadd  12879  mul4sq  12933  issubg2m  13742  dvdsrtr  14081  unitgrp  14096  subrgintm  14223  islssm  14337  znidom  14637  opnneiid  14854  txuni2  14946  txbas  14948  txbasval  14957  txlm  14969  blin2  15122  tgqioo  15245  plyadd  15441  plymul  15442  lgsquad2lem2  15777  2sqlem5  15814  uhgr2edg  16020  uspgr2wlkeq  16111  bj-charfunr  16256