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	⊢ (𝜓 ↔ 𝜑)
biimtrrid.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
biimtrrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem biimtrrid

Step	Hyp	Ref	Expression
1		biimtrrid.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 133	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 32	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  5522  funopfv  5673  mpteqb  5727  funfvima  5875  fliftfun  5926  iinerm  6762  eroveu  6781  th3qlem1  6792  updjudhf  7257  elni2  7512  genpdisj  7721  lttri3  8237  seqf1og  10755  nn0ltexp2  10943  zfz1iso  11076  ccatalpha  11161  cau3lem  11640  maxleast  11739  rexanre  11746  climcau  11873  summodc  11909  mertenslem2  12062  prodmodclem2  12103  prodmodc  12104  fprodseq  12109  bitsfzolem  12480  bitsfzo  12481  divgcdcoprmex  12639  prmind2  12657  pcqmul  12841  pcxcl  12849  pcadd  12878  mul4sq  12932  issubg2m  13741  dvdsrtr  14080  unitgrp  14095  subrgintm  14222  islssm  14336  znidom  14636  opnneiid  14853  txuni2  14945  txbas  14947  txbasval  14956  txlm  14968  blin2  15121  tgqioo  15244  plyadd  15440  plymul  15441  lgsquad2lem2  15776  2sqlem5  15813  uhgr2edg  16019  uspgr2wlkeq  16106  bj-charfunr  16228