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  1674  mo3h  2079  necon1bidc  2399  necon4aidc  2415  r19.30dc  2624  ceqex  2866  ssdisj  3481  ralidm  3525  exmid1dc  4202  rexxfrd  4465  sucprcreg  4550  imain  5300  f0rn0  5412  funopfv  5558  mpteqb  5609  funfvima  5751  fliftfun  5800  iinerm  6610  eroveu  6629  th3qlem1  6640  updjudhf  7081  elni2  7316  genpdisj  7525  lttri3  8040  nn0ltexp2  10692  zfz1iso  10824  cau3lem  11126  maxleast  11225  rexanre  11232  climcau  11358  summodc  11394  mertenslem2  11547  prodmodclem2  11588  prodmodc  11589  fprodseq  11594  divgcdcoprmex  12105  prmind2  12123  pcqmul  12306  pcxcl  12314  pcadd  12342  mul4sq  12395  issubg2m  13063  dvdsrtr  13308  unitgrp  13323  subrgintm  13402  opnneiid  13852  txuni2  13944  txbas  13946  txbasval  13955  txlm  13967  blin2  14120  tgqioo  14235  2sqlem5  14654  bj-charfunr  14750