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  1722  mo3h  2133  necon1bidc  2455  necon4aidc  2471  r19.30dc  2681  ceqex  2934  ssdisj  3553  ralidm  3597  exmid1dc  4296  rexxfrd  4566  sucprcreg  4653  imain  5419  f0rn0  5540  funopfv  5692  mpteqb  5746  funfvima  5896  fliftfun  5947  fvdifsuppst  6422  suppssrst  6439  suppssrgst  6440  iinerm  6819  eroveu  6838  th3qlem1  6849  updjudhf  7321  elni2  7577  genpdisj  7786  lttri3  8301  seqf1og  10829  nn0ltexp2  11017  zfz1iso  11151  ccatalpha  11239  cau3lem  11737  maxleast  11836  rexanre  11843  climcau  11970  summodc  12007  mertenslem2  12160  prodmodclem2  12201  prodmodc  12202  fprodseq  12207  bitsfzolem  12578  bitsfzo  12579  divgcdcoprmex  12737  prmind2  12755  pcqmul  12939  pcxcl  12947  pcadd  12976  mul4sq  13030  issubg2m  13839  dvdsrtr  14179  unitgrp  14194  subrgintm  14321  islssm  14436  znidom  14736  opnneiid  14958  txuni2  15050  txbas  15052  txbasval  15061  txlm  15073  blin2  15226  tgqioo  15349  plyadd  15545  plymul  15546  lgsquad2lem2  15884  2sqlem5  15921  uhgr2edg  16130  uspgr2wlkeq  16289  bj-charfunr  16509