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  2998  reupick  3507  prneimg  3880  invdisj  4104  trin  4220  exmidsssnc  4318  ordsucss  4628  eqbrrdva  4927  elreldm  4985  elres  5076  xp11m  5203  ssrnres  5207  opelf  5537  dffo4  5827  dftpos3  6495  tfr1onlemaccex  6581  tfrcllemaccex  6594  nnaordex  6763  swoer  6797  map0g  6924  mapsn  6927  nneneq  7113  fnfi  7205  prarloclemlo  7814  genprndl  7841  genprndu  7842  cauappcvgprlemladdrl  7977  caucvgprlemladdrl  7998  caucvgsrlemoffres  8120  caucvgsr  8122  nntopi  8214  letr  8361  reapcotr  8877  apcotr  8886  mulext1  8891  lt2msq  9165  nneoor  9686  xrletr  10147  icoshft  10329  swrdccatin2  11429  caucvgre  11674  absext  11756  rexico  11914  summodc  12077  gcdeq0  12681  intopsn  13601  znleval  14850  tgcn  15122  cnptoprest  15153  metequiv2  15410  bj-nnsn  16554  bj-inf2vnlem2  16790