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  6886  eroveu  6905  th3qlem1  6916  updjudhf  7425  elni2  7687  genpdisj  7896  lttri3  8411  seqf1og  10978  nn0ltexp2  11168  zfz1iso  11314  ccatalpha  11402  cau3lem  11902  maxleast  12001  rexanre  12008  climcau  12137  summodc  12174  mertenslem2  12327  prodmodclem2  12368  prodmodc  12369  fprodseq  12374  bitsfzolem  12745  bitsfzo  12746  divgcdcoprmex  12904  prmind2  12922  sqrtrirr  13013  pcqmul  13110  pcxcl  13118  pcadd  13147  mul4sq  13201  prmlem1a  13249  issubg2m  14050  dvdsrtr  14516  unitgrp  14531  subrgintm  14659  islssm  14802  znidom  15100  opnneiid  15407  txuni2  15499  txbas  15501  txbasval  15510  txlm  15522  blin2  15675  tgqioo  15798  plyadd  15994  plymul  15995  ppiublem1  16308  lgsquad2lem2  16423  2sqlem5  16460  uhgr2edg  16669  uspgr2wlkeq  16828  bj-charfunr  17058