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  1698  mo3h  2108  necon1bidc  2429  necon4aidc  2445  r19.30dc  2654  ceqex  2904  ssdisj  3521  ralidm  3565  exmid1dc  4252  rexxfrd  4518  sucprcreg  4605  imain  5365  f0rn0  5482  funopfv  5631  mpteqb  5683  funfvima  5829  fliftfun  5878  iinerm  6707  eroveu  6726  th3qlem1  6737  updjudhf  7196  elni2  7447  genpdisj  7656  lttri3  8172  seqf1og  10688  nn0ltexp2  10876  zfz1iso  11008  cau3lem  11500  maxleast  11599  rexanre  11606  climcau  11733  summodc  11769  mertenslem2  11922  prodmodclem2  11963  prodmodc  11964  fprodseq  11969  bitsfzolem  12340  bitsfzo  12341  divgcdcoprmex  12499  prmind2  12517  pcqmul  12701  pcxcl  12709  pcadd  12738  mul4sq  12792  issubg2m  13600  dvdsrtr  13938  unitgrp  13953  subrgintm  14080  islssm  14194  znidom  14494  opnneiid  14711  txuni2  14803  txbas  14805  txbasval  14814  txlm  14826  blin2  14979  tgqioo  15102  plyadd  15298  plymul  15299  lgsquad2lem2  15634  2sqlem5  15671  bj-charfunr  15884