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  1688  mo3h  2098  necon1bidc  2419  necon4aidc  2435  r19.30dc  2644  ceqex  2891  ssdisj  3507  ralidm  3551  exmid1dc  4233  rexxfrd  4498  sucprcreg  4585  imain  5340  f0rn0  5452  funopfv  5600  mpteqb  5652  funfvima  5794  fliftfun  5843  iinerm  6666  eroveu  6685  th3qlem1  6696  updjudhf  7145  elni2  7381  genpdisj  7590  lttri3  8106  seqf1og  10613  nn0ltexp2  10801  zfz1iso  10933  cau3lem  11279  maxleast  11378  rexanre  11385  climcau  11512  summodc  11548  mertenslem2  11701  prodmodclem2  11742  prodmodc  11743  fprodseq  11748  bitsfzolem  12118  bitsfzo  12119  divgcdcoprmex  12270  prmind2  12288  pcqmul  12472  pcxcl  12480  pcadd  12509  mul4sq  12563  issubg2m  13319  dvdsrtr  13657  unitgrp  13672  subrgintm  13799  islssm  13913  znidom  14213  opnneiid  14400  txuni2  14492  txbas  14494  txbasval  14503  txlm  14515  blin2  14668  tgqioo  14791  plyadd  14987  plymul  14988  lgsquad2lem2  15323  2sqlem5  15360  bj-charfunr  15456