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  2888  ssdisj  3504  ralidm  3548  exmid1dc  4230  rexxfrd  4495  sucprcreg  4582  imain  5337  f0rn0  5449  funopfv  5597  mpteqb  5649  funfvima  5791  fliftfun  5840  iinerm  6663  eroveu  6682  th3qlem1  6693  updjudhf  7140  elni2  7376  genpdisj  7585  lttri3  8101  seqf1og  10595  nn0ltexp2  10783  zfz1iso  10915  cau3lem  11261  maxleast  11360  rexanre  11367  climcau  11493  summodc  11529  mertenslem2  11682  prodmodclem2  11723  prodmodc  11724  fprodseq  11729  divgcdcoprmex  12243  prmind2  12261  pcqmul  12444  pcxcl  12452  pcadd  12481  mul4sq  12535  issubg2m  13262  dvdsrtr  13600  unitgrp  13615  subrgintm  13742  islssm  13856  znidom  14156  opnneiid  14343  txuni2  14435  txbas  14437  txbasval  14446  txlm  14458  blin2  14611  tgqioo  14734  plyadd  14930  plymul  14931  lgsquad2lem2  15239  2sqlem5  15276  bj-charfunr  15372