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  4508  sucprcreg  4595  imain  5350  f0rn0  5464  funopfv  5612  mpteqb  5664  funfvima  5806  fliftfun  5855  iinerm  6684  eroveu  6703  th3qlem1  6714  updjudhf  7163  elni2  7409  genpdisj  7618  lttri3  8134  seqf1og  10647  nn0ltexp2  10835  zfz1iso  10967  cau3lem  11344  maxleast  11443  rexanre  11450  climcau  11577  summodc  11613  mertenslem2  11766  prodmodclem2  11807  prodmodc  11808  fprodseq  11813  bitsfzolem  12184  bitsfzo  12185  divgcdcoprmex  12343  prmind2  12361  pcqmul  12545  pcxcl  12553  pcadd  12582  mul4sq  12636  issubg2m  13443  dvdsrtr  13781  unitgrp  13796  subrgintm  13923  islssm  14037  znidom  14337  opnneiid  14554  txuni2  14646  txbas  14648  txbasval  14657  txlm  14669  blin2  14822  tgqioo  14945  plyadd  15141  plymul  15142  lgsquad2lem2  15477  2sqlem5  15514  bj-charfunr  15610