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  1685  mo3h  2095  necon1bidc  2416  necon4aidc  2432  r19.30dc  2641  ceqex  2887  ssdisj  3503  ralidm  3547  exmid1dc  4229  rexxfrd  4494  sucprcreg  4581  imain  5336  f0rn0  5448  funopfv  5596  mpteqb  5648  funfvima  5790  fliftfun  5839  iinerm  6661  eroveu  6680  th3qlem1  6691  updjudhf  7138  elni2  7374  genpdisj  7583  lttri3  8099  seqf1og  10592  nn0ltexp2  10780  zfz1iso  10912  cau3lem  11258  maxleast  11357  rexanre  11364  climcau  11490  summodc  11526  mertenslem2  11679  prodmodclem2  11720  prodmodc  11721  fprodseq  11726  divgcdcoprmex  12240  prmind2  12258  pcqmul  12441  pcxcl  12449  pcadd  12478  mul4sq  12532  issubg2m  13259  dvdsrtr  13597  unitgrp  13612  subrgintm  13739  islssm  13853  znidom  14145  opnneiid  14332  txuni2  14424  txbas  14426  txbasval  14435  txlm  14447  blin2  14600  tgqioo  14715  plyadd  14897  plymul  14898  2sqlem5  15206  bj-charfunr  15302