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  1674  mo3h  2079  necon1bidc  2399  necon4aidc  2415  r19.30dc  2624  ceqex  2866  ssdisj  3481  ralidm  3525  exmid1dc  4202  rexxfrd  4465  sucprcreg  4550  imain  5300  f0rn0  5412  funopfv  5557  mpteqb  5608  funfvima  5750  fliftfun  5799  iinerm  6609  eroveu  6628  th3qlem1  6639  updjudhf  7080  elni2  7315  genpdisj  7524  lttri3  8039  nn0ltexp2  10691  zfz1iso  10823  cau3lem  11125  maxleast  11224  rexanre  11231  climcau  11357  summodc  11393  mertenslem2  11546  prodmodclem2  11587  prodmodc  11588  fprodseq  11593  divgcdcoprmex  12104  prmind2  12122  pcqmul  12305  pcxcl  12313  pcadd  12341  mul4sq  12394  issubg2m  13054  dvdsrtr  13275  unitgrp  13290  subrgintm  13369  opnneiid  13703  txuni2  13795  txbas  13797  txbasval  13806  txlm  13818  blin2  13971  tgqioo  14086  2sqlem5  14505  bj-charfunr  14601