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  1726  mo3h  2140  necon1bidc  2472  necon4aidc  2488  r19.30dc  2698  ceqex  2953  ssdisj  3580  ralidm  3625  exmid1dc  4332  rexxfrd  4604  sucprcreg  4691  imain  5458  f0rn0  5582  funopfv  5734  mpteqb  5790  funfvima  5940  fliftfun  5992  fvdifsuppst  6474  suppssrst  6491  suppssrgst  6492  iinerm  6871  eroveu  6890  th3qlem1  6901  updjudhf  7409  elni2  7671  genpdisj  7880  lttri3  8395  seqf1og  10936  nn0ltexp2  11125  zfz1iso  11271  ccatalpha  11359  cau3lem  11858  maxleast  11957  rexanre  11964  climcau  12091  summodc  12128  mertenslem2  12281  prodmodclem2  12322  prodmodc  12323  fprodseq  12328  bitsfzolem  12699  bitsfzo  12700  divgcdcoprmex  12858  prmind2  12876  pcqmul  13060  pcxcl  13068  pcadd  13097  mul4sq  13151  issubg2m  13969  dvdsrtr  14381  unitgrp  14396  subrgintm  14524  islssm  14666  znidom  14964  opnneiid  15188  txuni2  15280  txbas  15282  txbasval  15291  txlm  15303  blin2  15456  tgqioo  15579  plyadd  15775  plymul  15776  lgsquad2lem2  16115  2sqlem5  16152  uhgr2edg  16361  uspgr2wlkeq  16520  bj-charfunr  16750