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  1722  mo3h  2133  necon1bidc  2455  necon4aidc  2471  r19.30dc  2681  ceqex  2934  ssdisj  3553  ralidm  3597  exmid1dc  4296  rexxfrd  4566  sucprcreg  4653  imain  5419  f0rn0  5540  funopfv  5692  mpteqb  5746  funfvima  5896  fliftfun  5947  fvdifsuppst  6422  suppssrst  6439  suppssrgst  6440  iinerm  6819  eroveu  6838  th3qlem1  6849  updjudhf  7338  elni2  7594  genpdisj  7803  lttri3  8318  seqf1og  10846  nn0ltexp2  11034  zfz1iso  11168  ccatalpha  11256  cau3lem  11754  maxleast  11853  rexanre  11860  climcau  11987  summodc  12024  mertenslem2  12177  prodmodclem2  12218  prodmodc  12219  fprodseq  12224  bitsfzolem  12595  bitsfzo  12596  divgcdcoprmex  12754  prmind2  12772  pcqmul  12956  pcxcl  12964  pcadd  12993  mul4sq  13047  issubg2m  13856  dvdsrtr  14196  unitgrp  14211  subrgintm  14338  islssm  14453  znidom  14753  opnneiid  14975  txuni2  15067  txbas  15069  txbasval  15078  txlm  15090  blin2  15243  tgqioo  15366  plyadd  15562  plymul  15563  lgsquad2lem2  15901  2sqlem5  15938  uhgr2edg  16147  uspgr2wlkeq  16306  bj-charfunr  16526