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  888  nfalt  1627  alexim  1694  19.36-1  1721  ax11ev  1877  equs5or  1879  necon2bd  2472  necon2d  2473  necon1bbiddc  2477  necon2abiddc  2480  necon2bbiddc  2481  necon4idc  2483  necon4ddc  2486  necon1bddc  2491  spc2gv  2910  spc3gv  2912  mo2icl  2999  reupick  3509  prneimg  3883  invdisj  4107  trin  4223  exmidsssnc  4321  ordsucss  4631  eqbrrdva  4930  elreldm  4988  elres  5079  xp11m  5206  ssrnres  5210  opelf  5540  dffo4  5830  dftpos3  6506  tfr1onlemaccex  6592  tfrcllemaccex  6605  nnaordex  6774  swoer  6808  map0g  6935  mapsn  6938  nneneq  7124  fnfi  7216  prarloclemlo  7825  genprndl  7852  genprndu  7853  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgsrlemoffres  8131  caucvgsr  8133  nntopi  8225  letr  8372  reapcotr  8890  apcotr  8899  mulext1  8904  lt2msq  9180  nneoor  9701  xrletr  10163  icoshft  10345  swrdccatin2  11449  caucvgre  11694  absext  11776  rexico  11934  summodc  12097  gcdeq0  12701  intopsn  13633  znleval  14930  tgcn  15202  cnptoprest  15233  metequiv2  15490  bj-nnsn  16644  bj-inf2vnlem2  16880