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  4337  rexxfrd  4609  sucprcreg  4696  imain  5463  f0rn0  5587  funopfv  5740  mpteqb  5796  funfvima  5950  fliftfun  6002  fvdifsuppst  6484  suppssrst  6501  suppssrgst  6502  iinerm  6881  eroveu  6900  th3qlem1  6911  updjudhf  7419  elni2  7681  genpdisj  7890  lttri3  8405  seqf1og  10971  nn0ltexp2  11161  zfz1iso  11307  ccatalpha  11395  cau3lem  11895  maxleast  11994  rexanre  12001  climcau  12129  summodc  12166  mertenslem2  12319  prodmodclem2  12360  prodmodc  12361  fprodseq  12366  bitsfzolem  12737  bitsfzo  12738  divgcdcoprmex  12896  prmind2  12914  sqrtrirr  13005  pcqmul  13102  pcxcl  13110  pcadd  13139  mul4sq  13193  prmlem1a  13241  issubg2m  14041  dvdsrtr  14457  unitgrp  14472  subrgintm  14600  islssm  14743  znidom  15041  opnneiid  15314  txuni2  15406  txbas  15408  txbasval  15417  txlm  15429  blin2  15582  tgqioo  15705  plyadd  15901  plymul  15902  ppiublem1  16192  lgsquad2lem2  16299  2sqlem5  16336  uhgr2edg  16545  uspgr2wlkeq  16704  bj-charfunr  16934