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  1685  mo3h  2091  necon1bidc  2412  necon4aidc  2428  r19.30dc  2637  ceqex  2883  ssdisj  3498  ralidm  3542  exmid1dc  4225  rexxfrd  4488  sucprcreg  4573  imain  5324  f0rn0  5436  funopfv  5583  mpteqb  5634  funfvima  5776  fliftfun  5825  iinerm  6641  eroveu  6660  th3qlem1  6671  updjudhf  7117  elni2  7353  genpdisj  7562  lttri3  8078  nn0ltexp2  10736  zfz1iso  10868  cau3lem  11170  maxleast  11269  rexanre  11276  climcau  11402  summodc  11438  mertenslem2  11591  prodmodclem2  11632  prodmodc  11633  fprodseq  11638  divgcdcoprmex  12151  prmind2  12169  pcqmul  12352  pcxcl  12360  pcadd  12389  mul4sq  12443  issubg2m  13161  dvdsrtr  13488  unitgrp  13503  subrgintm  13627  islssm  13716  opnneiid  14185  txuni2  14277  txbas  14279  txbasval  14288  txlm  14300  blin2  14453  tgqioo  14568  2sqlem5  15005  bj-charfunr  15101