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  1696  mo3h  2106  necon1bidc  2427  necon4aidc  2443  r19.30dc  2652  ceqex  2899  ssdisj  3516  ralidm  3560  exmid1dc  4243  rexxfrd  4509  sucprcreg  4596  imain  5355  f0rn0  5469  funopfv  5617  mpteqb  5669  funfvima  5815  fliftfun  5864  iinerm  6693  eroveu  6712  th3qlem1  6723  updjudhf  7180  elni2  7426  genpdisj  7635  lttri3  8151  seqf1og  10664  nn0ltexp2  10852  zfz1iso  10984  cau3lem  11367  maxleast  11466  rexanre  11473  climcau  11600  summodc  11636  mertenslem2  11789  prodmodclem2  11830  prodmodc  11831  fprodseq  11836  bitsfzolem  12207  bitsfzo  12208  divgcdcoprmex  12366  prmind2  12384  pcqmul  12568  pcxcl  12576  pcadd  12605  mul4sq  12659  issubg2m  13467  dvdsrtr  13805  unitgrp  13820  subrgintm  13947  islssm  14061  znidom  14361  opnneiid  14578  txuni2  14670  txbas  14672  txbasval  14681  txlm  14693  blin2  14846  tgqioo  14969  plyadd  15165  plymul  15166  lgsquad2lem2  15501  2sqlem5  15538  bj-charfunr  15679