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  1722  mo3h  2134  necon1bidc  2464  necon4aidc  2480  r19.30dc  2690  ceqex  2944  ssdisj  3565  ralidm  3610  exmid1dc  4313  rexxfrd  4584  sucprcreg  4671  imain  5438  f0rn0  5562  funopfv  5714  mpteqb  5768  funfvima  5918  fliftfun  5969  fvdifsuppst  6444  suppssrst  6461  suppssrgst  6462  iinerm  6841  eroveu  6860  th3qlem1  6871  updjudhf  7370  elni2  7629  genpdisj  7838  lttri3  8353  seqf1og  10883  nn0ltexp2  11071  zfz1iso  11213  ccatalpha  11301  cau3lem  11799  maxleast  11898  rexanre  11905  climcau  12032  summodc  12069  mertenslem2  12222  prodmodclem2  12263  prodmodc  12264  fprodseq  12269  bitsfzolem  12640  bitsfzo  12641  divgcdcoprmex  12799  prmind2  12817  pcqmul  13001  pcxcl  13009  pcadd  13038  mul4sq  13092  issubg2m  13906  dvdsrtr  14246  unitgrp  14261  subrgintm  14388  islssm  14505  znidom  14805  opnneiid  15029  txuni2  15121  txbas  15123  txbasval  15132  txlm  15144  blin2  15297  tgqioo  15420  plyadd  15616  plymul  15617  lgsquad2lem2  15955  2sqlem5  15992  uhgr2edg  16201  uspgr2wlkeq  16360  bj-charfunr  16580