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  4244  rexxfrd  4510  sucprcreg  4597  imain  5356  f0rn0  5470  funopfv  5618  mpteqb  5670  funfvima  5816  fliftfun  5865  iinerm  6694  eroveu  6713  th3qlem1  6724  updjudhf  7181  elni2  7427  genpdisj  7636  lttri3  8152  seqf1og  10666  nn0ltexp2  10854  zfz1iso  10986  cau3lem  11425  maxleast  11524  rexanre  11531  climcau  11658  summodc  11694  mertenslem2  11847  prodmodclem2  11888  prodmodc  11889  fprodseq  11894  bitsfzolem  12265  bitsfzo  12266  divgcdcoprmex  12424  prmind2  12442  pcqmul  12626  pcxcl  12634  pcadd  12663  mul4sq  12717  issubg2m  13525  dvdsrtr  13863  unitgrp  13878  subrgintm  14005  islssm  14119  znidom  14419  opnneiid  14636  txuni2  14728  txbas  14730  txbasval  14739  txlm  14751  blin2  14904  tgqioo  15027  plyadd  15223  plymul  15224  lgsquad2lem2  15559  2sqlem5  15596  bj-charfunr  15746