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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3g  204  19.37-1  1726  mo3h  2140  necon1bidc  2472  necon4aidc  2488  r19.30dc  2698  ceqex  2953  ssdisj  3581  ralidm  3628  exmid1dc  4339  rexxfrd  4611  sucprcreg  4698  imain  5466  f0rn0  5590  funopfv  5743  mpteqb  5799  funfvima  5953  fliftfun  6005  fvdifsuppst  6488  suppssrst  6505  suppssrgst  6506  iinerm  6885  eroveu  6904  th3qlem1  6915  updjudhf  7425  elni2  7687  genpdisj  7896  lttri3  8411  seqf1og  10979  nn0ltexp2  11169  zfz1iso  11315  ccatalpha  11403  cau3lem  11903  maxleast  12002  rexanre  12009  climcau  12138  summodc  12175  mertenslem2  12328  prodmodclem2  12369  prodmodc  12370  fprodseq  12375  bitsfzolem  12746  bitsfzo  12747  divgcdcoprmex  12905  prmind2  12923  sqrtrirr  13014  pcqmul  13111  pcxcl  13119  pcadd  13148  mul4sq  13202  prmlem1a  13250  issubg2m  14051  dvdsrtr  14517  unitgrp  14532  subrgintm  14660  islssm  14803  znidom  15101  opnneiid  15390  txuni2  15482  txbas  15484  txbasval  15493  txlm  15505  blin2  15658  tgqioo  15781  plyadd  15977  plymul  15978  ppiublem1  16291  lgsquad2lem2  16406  2sqlem5  16443  uhgr2edg  16652  uspgr2wlkeq  16811  bj-charfunr  17041