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  1697  mo3h  2107  necon1bidc  2428  necon4aidc  2444  r19.30dc  2653  ceqex  2900  ssdisj  3517  ralidm  3561  exmid1dc  4245  rexxfrd  4511  sucprcreg  4598  imain  5357  f0rn0  5472  funopfv  5620  mpteqb  5672  funfvima  5818  fliftfun  5867  iinerm  6696  eroveu  6715  th3qlem1  6726  updjudhf  7183  elni2  7429  genpdisj  7638  lttri3  8154  seqf1og  10668  nn0ltexp2  10856  zfz1iso  10988  cau3lem  11458  maxleast  11557  rexanre  11564  climcau  11691  summodc  11727  mertenslem2  11880  prodmodclem2  11921  prodmodc  11922  fprodseq  11927  bitsfzolem  12298  bitsfzo  12299  divgcdcoprmex  12457  prmind2  12475  pcqmul  12659  pcxcl  12667  pcadd  12696  mul4sq  12750  issubg2m  13558  dvdsrtr  13896  unitgrp  13911  subrgintm  14038  islssm  14152  znidom  14452  opnneiid  14669  txuni2  14761  txbas  14763  txbasval  14772  txlm  14784  blin2  14937  tgqioo  15060  plyadd  15256  plymul  15257  lgsquad2lem2  15592  2sqlem5  15629  bj-charfunr  15783