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  1688  mo3h  2098  necon1bidc  2419  necon4aidc  2435  r19.30dc  2644  ceqex  2891  ssdisj  3508  ralidm  3552  exmid1dc  4234  rexxfrd  4499  sucprcreg  4586  imain  5341  f0rn0  5455  funopfv  5603  mpteqb  5655  funfvima  5797  fliftfun  5846  iinerm  6675  eroveu  6694  th3qlem1  6705  updjudhf  7154  elni2  7400  genpdisj  7609  lttri3  8125  seqf1og  10632  nn0ltexp2  10820  zfz1iso  10952  cau3lem  11298  maxleast  11397  rexanre  11404  climcau  11531  summodc  11567  mertenslem2  11720  prodmodclem2  11761  prodmodc  11762  fprodseq  11767  bitsfzolem  12138  bitsfzo  12139  divgcdcoprmex  12297  prmind2  12315  pcqmul  12499  pcxcl  12507  pcadd  12536  mul4sq  12590  issubg2m  13397  dvdsrtr  13735  unitgrp  13750  subrgintm  13877  islssm  13991  znidom  14291  opnneiid  14508  txuni2  14600  txbas  14602  txbasval  14611  txlm  14623  blin2  14776  tgqioo  14899  plyadd  15095  plymul  15096  lgsquad2lem2  15431  2sqlem5  15468  bj-charfunr  15564