Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl6ib GIF version

Theorem syl6ib 160
 Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ib.1 (𝜑 → (𝜓𝜒))
syl6ib.2 (𝜒𝜃)
Assertion
Ref Expression
syl6ib (𝜑 → (𝜓𝜃))

Proof of Theorem syl6ib
StepHypRef Expression
1 syl6ib.1 . 2 (𝜑 → (𝜓𝜒))
2 syl6ib.2 . . 3 (𝜒𝜃)
32biimpi 119 . 2 (𝜒𝜃)
41, 3syl6 33 1 (𝜑 → (𝜓𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  3imtr3g  203  exp4a  364  con2biddc  866  nfalt  1558  alexim  1625  19.36-1  1652  ax11ev  1801  equs5or  1803  necon2bd  2367  necon2d  2368  necon1bbiddc  2372  necon2abiddc  2375  necon2bbiddc  2376  necon4idc  2378  necon4ddc  2381  necon1bddc  2386  spc2gv  2779  spc3gv  2781  mo2icl  2866  reupick  3364  prneimg  3708  invdisj  3930  trin  4043  exmidsssnc  4133  ordsucss  4427  eqbrrdva  4716  elreldm  4772  elres  4862  xp11m  4984  ssrnres  4988  opelf  5301  dffo4  5575  dftpos3  6166  tfr1onlemaccex  6252  tfrcllemaccex  6265  nnaordex  6430  swoer  6464  map0g  6589  mapsn  6591  nneneq  6758  fnfi  6832  prarloclemlo  7325  genprndl  7352  genprndu  7353  cauappcvgprlemladdrl  7488  caucvgprlemladdrl  7509  caucvgsrlemoffres  7631  caucvgsr  7633  nntopi  7725  letr  7870  reapcotr  8383  apcotr  8392  mulext1  8397  cnstab  8430  lt2msq  8667  nneoor  9176  xrletr  9620  icoshft  9802  caucvgre  10784  absext  10866  rexico  11024  summodc  11183  gcdeq0  11699  tgcn  12414  cnptoprest  12445  metequiv2  12702  bj-nnsn  13114  bj-inf2vnlem2  13338
 Copyright terms: Public domain W3C validator