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 ⊢ (𝜒 → (𝜑 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  3imtr3g  204  19.37-1  1726  mo3h  2140  necon1bidc  2472  necon4aidc  2488  r19.30dc  2698  ceqex  2953  ssdisj  3581  ralidm  3628  exmid1dc  4337  rexxfrd  4609  sucprcreg  4696  imain  5463  f0rn0  5587  funopfv  5740  mpteqb  5796  funfvima  5950  fliftfun  6002  fvdifsuppst  6484  suppssrst  6501  suppssrgst  6502  iinerm  6881  eroveu  6900  th3qlem1  6911  updjudhf  7419  elni2  7681  genpdisj  7890  lttri3  8405  seqf1og  10958  nn0ltexp2  11147  zfz1iso  11293  ccatalpha  11381  cau3lem  11880  maxleast  11979  rexanre  11986  climcau  12113  summodc  12150  mertenslem2  12303  prodmodclem2  12344  prodmodc  12345  fprodseq  12350  bitsfzolem  12721  bitsfzo  12722  divgcdcoprmex  12880  prmind2  12898  pcqmul  13082  pcxcl  13090  pcadd  13119  mul4sq  13173  issubg2m  13992  dvdsrtr  14408  unitgrp  14423  subrgintm  14551  islssm  14694  znidom  14992  opnneiid  15265  txuni2  15357  txbas  15359  txbasval  15368  txlm  15380  blin2  15533  tgqioo  15656  plyadd  15852  plymul  15853  lgsquad2lem2  16201  2sqlem5  16238  uhgr2edg  16447  uspgr2wlkeq  16606  bj-charfunr  16836