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  4283  rexxfrd  4553  sucprcreg  4640  imain  5402  f0rn0  5519  funopfv  5670  mpteqb  5724  funfvima  5870  fliftfun  5919  iinerm  6752  eroveu  6771  th3qlem1  6782  updjudhf  7242  elni2  7497  genpdisj  7706  lttri3  8222  seqf1og  10738  nn0ltexp2  10926  zfz1iso  11058  cau3lem  11620  maxleast  11719  rexanre  11726  climcau  11853  summodc  11889  mertenslem2  12042  prodmodclem2  12083  prodmodc  12084  fprodseq  12089  bitsfzolem  12460  bitsfzo  12461  divgcdcoprmex  12619  prmind2  12637  pcqmul  12821  pcxcl  12829  pcadd  12858  mul4sq  12912  issubg2m  13721  dvdsrtr  14059  unitgrp  14074  subrgintm  14201  islssm  14315  znidom  14615  opnneiid  14832  txuni2  14924  txbas  14926  txbasval  14935  txlm  14947  blin2  15100  tgqioo  15223  plyadd  15419  plymul  15420  lgsquad2lem2  15755  2sqlem5  15792  uhgr2edg  15998  bj-charfunr  16131