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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3g  204  19.37-1  1726  mo3h  2140  necon1bidc  2472  necon4aidc  2488  r19.30dc  2698  ceqex  2953  ssdisj  3581  ralidm  3628  exmid1dc  4337  rexxfrd  4609  sucprcreg  4696  imain  5463  f0rn0  5587  funopfv  5740  mpteqb  5796  funfvima  5950  fliftfun  6002  fvdifsuppst  6484  suppssrst  6501  suppssrgst  6502  iinerm  6881  eroveu  6900  th3qlem1  6911  updjudhf  7420  elni2  7682  genpdisj  7891  lttri3  8406  seqf1og  10973  nn0ltexp2  11163  zfz1iso  11309  ccatalpha  11397  cau3lem  11897  maxleast  11996  rexanre  12003  climcau  12132  summodc  12169  mertenslem2  12322  prodmodclem2  12363  prodmodc  12364  fprodseq  12369  bitsfzolem  12740  bitsfzo  12741  divgcdcoprmex  12899  prmind2  12917  sqrtrirr  13008  pcqmul  13105  pcxcl  13113  pcadd  13142  mul4sq  13196  prmlem1a  13244  issubg2m  14045  dvdsrtr  14492  unitgrp  14507  subrgintm  14635  islssm  14778  znidom  15076  opnneiid  15356  txuni2  15448  txbas  15450  txbasval  15459  txlm  15471  blin2  15624  tgqioo  15747  plyadd  15943  plymul  15944  ppiublem1  16252  lgsquad2lem2  16367  2sqlem5  16404  uhgr2edg  16613  uspgr2wlkeq  16772  bj-charfunr  17002