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  1698  mo3h  2109  necon1bidc  2430  necon4aidc  2446  r19.30dc  2655  ceqex  2907  ssdisj  3525  ralidm  3569  exmid1dc  4260  rexxfrd  4528  sucprcreg  4615  imain  5375  f0rn0  5492  funopfv  5641  mpteqb  5693  funfvima  5839  fliftfun  5888  iinerm  6717  eroveu  6736  th3qlem1  6747  updjudhf  7207  elni2  7462  genpdisj  7671  lttri3  8187  seqf1og  10703  nn0ltexp2  10891  zfz1iso  11023  cau3lem  11540  maxleast  11639  rexanre  11646  climcau  11773  summodc  11809  mertenslem2  11962  prodmodclem2  12003  prodmodc  12004  fprodseq  12009  bitsfzolem  12380  bitsfzo  12381  divgcdcoprmex  12539  prmind2  12557  pcqmul  12741  pcxcl  12749  pcadd  12778  mul4sq  12832  issubg2m  13640  dvdsrtr  13978  unitgrp  13993  subrgintm  14120  islssm  14234  znidom  14534  opnneiid  14751  txuni2  14843  txbas  14845  txbasval  14854  txlm  14866  blin2  15019  tgqioo  15142  plyadd  15338  plymul  15339  lgsquad2lem2  15674  2sqlem5  15711  bj-charfunr  15945