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  1688  mo3h  2098  necon1bidc  2419  necon4aidc  2435  r19.30dc  2644  ceqex  2891  ssdisj  3508  ralidm  3552  exmid1dc  4234  rexxfrd  4499  sucprcreg  4586  imain  5341  f0rn0  5455  funopfv  5603  mpteqb  5655  funfvima  5797  fliftfun  5846  iinerm  6675  eroveu  6694  th3qlem1  6705  updjudhf  7154  elni2  7398  genpdisj  7607  lttri3  8123  seqf1og  10630  nn0ltexp2  10818  zfz1iso  10950  cau3lem  11296  maxleast  11395  rexanre  11402  climcau  11529  summodc  11565  mertenslem2  11718  prodmodclem2  11759  prodmodc  11760  fprodseq  11765  bitsfzolem  12136  bitsfzo  12137  divgcdcoprmex  12295  prmind2  12313  pcqmul  12497  pcxcl  12505  pcadd  12534  mul4sq  12588  issubg2m  13395  dvdsrtr  13733  unitgrp  13748  subrgintm  13875  islssm  13989  znidom  14289  opnneiid  14484  txuni2  14576  txbas  14578  txbasval  14587  txlm  14599  blin2  14752  tgqioo  14875  plyadd  15071  plymul  15072  lgsquad2lem2  15407  2sqlem5  15444  bj-charfunr  15540