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  2864  ssdisj  3479  ralidm  3523  exmid1dc  4200  rexxfrd  4463  sucprcreg  4548  imain  5298  f0rn0  5410  funopfv  5555  mpteqb  5606  funfvima  5748  fliftfun  5796  iinerm  6606  eroveu  6625  th3qlem1  6636  updjudhf  7077  elni2  7312  genpdisj  7521  lttri3  8036  nn0ltexp2  10688  zfz1iso  10820  cau3lem  11122  maxleast  11221  rexanre  11228  climcau  11354  summodc  11390  mertenslem2  11543  prodmodclem2  11584  prodmodc  11585  fprodseq  11590  divgcdcoprmex  12101  prmind2  12119  pcqmul  12302  pcxcl  12310  pcadd  12338  mul4sq  12391  issubg2m  13047  dvdsrtr  13268  unitgrp  13283  subrgintm  13362  opnneiid  13634  txuni2  13726  txbas  13728  txbasval  13737  txlm  13749  blin2  13902  tgqioo  14017  2sqlem5  14436  bj-charfunr  14532