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  1684  mo3h  2090  necon1bidc  2411  necon4aidc  2427  r19.30dc  2636  ceqex  2878  ssdisj  3493  ralidm  3537  exmid1dc  4214  rexxfrd  4477  sucprcreg  4562  imain  5312  f0rn0  5424  funopfv  5570  mpteqb  5621  funfvima  5763  fliftfun  5812  iinerm  6624  eroveu  6643  th3qlem1  6654  updjudhf  7095  elni2  7330  genpdisj  7539  lttri3  8054  nn0ltexp2  10706  zfz1iso  10838  cau3lem  11140  maxleast  11239  rexanre  11246  climcau  11372  summodc  11408  mertenslem2  11561  prodmodclem2  11602  prodmodc  11603  fprodseq  11608  divgcdcoprmex  12119  prmind2  12137  pcqmul  12320  pcxcl  12328  pcadd  12356  mul4sq  12409  issubg2m  13093  dvdsrtr  13411  unitgrp  13426  subrgintm  13550  islssm  13633  opnneiid  14047  txuni2  14139  txbas  14141  txbasval  14150  txlm  14162  blin2  14315  tgqioo  14430  2sqlem5  14849  bj-charfunr  14945