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  1720  mo3h  2131  necon1bidc  2452  necon4aidc  2468  r19.30dc  2678  ceqex  2931  ssdisj  3549  ralidm  3593  exmid1dc  4288  rexxfrd  4558  sucprcreg  4645  imain  5409  f0rn0  5528  funopfv  5679  mpteqb  5733  funfvima  5881  fliftfun  5932  iinerm  6771  eroveu  6790  th3qlem1  6801  updjudhf  7269  elni2  7524  genpdisj  7733  lttri3  8249  seqf1og  10773  nn0ltexp2  10961  zfz1iso  11095  ccatalpha  11180  cau3lem  11665  maxleast  11764  rexanre  11771  climcau  11898  summodc  11934  mertenslem2  12087  prodmodclem2  12128  prodmodc  12129  fprodseq  12134  bitsfzolem  12505  bitsfzo  12506  divgcdcoprmex  12664  prmind2  12682  pcqmul  12866  pcxcl  12874  pcadd  12903  mul4sq  12957  issubg2m  13766  dvdsrtr  14105  unitgrp  14120  subrgintm  14247  islssm  14361  znidom  14661  opnneiid  14878  txuni2  14970  txbas  14972  txbasval  14981  txlm  14993  blin2  15146  tgqioo  15269  plyadd  15465  plymul  15466  lgsquad2lem2  15801  2sqlem5  15838  uhgr2edg  16045  uspgr2wlkeq  16162  bj-charfunr  16341