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  2133  necon1bidc  2454  necon4aidc  2470  r19.30dc  2680  ceqex  2933  ssdisj  3551  ralidm  3595  exmid1dc  4290  rexxfrd  4560  sucprcreg  4647  imain  5412  f0rn0  5531  funopfv  5683  mpteqb  5737  funfvima  5885  fliftfun  5936  iinerm  6775  eroveu  6794  th3qlem1  6805  updjudhf  7277  elni2  7533  genpdisj  7742  lttri3  8258  seqf1og  10782  nn0ltexp2  10970  zfz1iso  11104  ccatalpha  11189  cau3lem  11674  maxleast  11773  rexanre  11780  climcau  11907  summodc  11943  mertenslem2  12096  prodmodclem2  12137  prodmodc  12138  fprodseq  12143  bitsfzolem  12514  bitsfzo  12515  divgcdcoprmex  12673  prmind2  12691  pcqmul  12875  pcxcl  12883  pcadd  12912  mul4sq  12966  issubg2m  13775  dvdsrtr  14114  unitgrp  14129  subrgintm  14256  islssm  14370  znidom  14670  opnneiid  14887  txuni2  14979  txbas  14981  txbasval  14990  txlm  15002  blin2  15155  tgqioo  15278  plyadd  15474  plymul  15475  lgsquad2lem2  15810  2sqlem5  15847  uhgr2edg  16056  uspgr2wlkeq  16215  bj-charfunr  16405