Theorem imbitrdi 161

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
imbitrdi.1	⊢ (𝜑 → (𝜓 → 𝜒))
imbitrdi.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
imbitrdi	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem imbitrdi

Step	Hyp	Ref	Expression
1		imbitrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 120	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 33	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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3imtr3g  204  exp4a  366  con2biddc  881  nfalt  1592  alexim  1659  19.36-1  1687  ax11ev  1842  equs5or  1844  necon2bd  2425  necon2d  2426  necon1bbiddc  2430  necon2abiddc  2433  necon2bbiddc  2434  necon4idc  2436  necon4ddc  2439  necon1bddc  2444  spc2gv  2855  spc3gv  2857  mo2icl  2943  reupick  3447  prneimg  3804  invdisj  4027  trin  4141  exmidsssnc  4236  ordsucss  4540  eqbrrdva  4836  elreldm  4892  elres  4982  xp11m  5108  ssrnres  5112  opelf  5429  dffo4  5710  dftpos3  6320  tfr1onlemaccex  6406  tfrcllemaccex  6419  nnaordex  6586  swoer  6620  map0g  6747  mapsn  6749  nneneq  6918  fnfi  7002  prarloclemlo  7561  genprndl  7588  genprndu  7589  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgsrlemoffres  7867  caucvgsr  7869  nntopi  7961  letr  8109  reapcotr  8625  apcotr  8634  mulext1  8639  lt2msq  8913  nneoor  9428  xrletr  9883  icoshft  10065  caucvgre  11146  absext  11228  rexico  11386  summodc  11548  gcdeq0  12144  intopsn  13010  znleval  14209  tgcn  14444  cnptoprest  14475  metequiv2  14732  bj-nnsn  15379  bj-inf2vnlem2  15617