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  1720  mo3h  2131  necon1bidc  2452  necon4aidc  2468  r19.30dc  2678  ceqex  2930  ssdisj  3548  ralidm  3592  exmid1dc  4284  rexxfrd  4554  sucprcreg  4641  imain  5403  f0rn0  5520  funopfv  5671  mpteqb  5725  funfvima  5871  fliftfun  5920  iinerm  6754  eroveu  6773  th3qlem1  6784  updjudhf  7246  elni2  7501  genpdisj  7710  lttri3  8226  seqf1og  10743  nn0ltexp2  10931  zfz1iso  11063  cau3lem  11625  maxleast  11724  rexanre  11731  climcau  11858  summodc  11894  mertenslem2  12047  prodmodclem2  12088  prodmodc  12089  fprodseq  12094  bitsfzolem  12465  bitsfzo  12466  divgcdcoprmex  12624  prmind2  12642  pcqmul  12826  pcxcl  12834  pcadd  12863  mul4sq  12917  issubg2m  13726  dvdsrtr  14065  unitgrp  14080  subrgintm  14207  islssm  14321  znidom  14621  opnneiid  14838  txuni2  14930  txbas  14932  txbasval  14941  txlm  14953  blin2  15106  tgqioo  15229  plyadd  15425  plymul  15426  lgsquad2lem2  15761  2sqlem5  15798  uhgr2edg  16004  uspgr2wlkeq  16076  bj-charfunr  16173