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  2454  necon4aidc  2470  r19.30dc  2680  ceqex  2933  ssdisj  3551  ralidm  3595  exmid1dc  4290  rexxfrd  4560  sucprcreg  4647  imain  5412  f0rn0  5531  funopfv  5683  mpteqb  5737  funfvima  5886  fliftfun  5937  iinerm  6776  eroveu  6795  th3qlem1  6806  updjudhf  7278  elni2  7534  genpdisj  7743  lttri3  8259  seqf1og  10784  nn0ltexp2  10972  zfz1iso  11106  ccatalpha  11194  cau3lem  11692  maxleast  11791  rexanre  11798  climcau  11925  summodc  11962  mertenslem2  12115  prodmodclem2  12156  prodmodc  12157  fprodseq  12162  bitsfzolem  12533  bitsfzo  12534  divgcdcoprmex  12692  prmind2  12710  pcqmul  12894  pcxcl  12902  pcadd  12931  mul4sq  12985  issubg2m  13794  dvdsrtr  14134  unitgrp  14149  subrgintm  14276  islssm  14390  znidom  14690  opnneiid  14907  txuni2  14999  txbas  15001  txbasval  15010  txlm  15022  blin2  15175  tgqioo  15298  plyadd  15494  plymul  15495  lgsquad2lem2  15830  2sqlem5  15867  uhgr2edg  16076  uspgr2wlkeq  16235  bj-charfunr  16456