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

Theorem syl6ib 159
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 118 . 2 (𝜒𝜃)
41, 3syl6 33 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3imtr3g  202  exp4a  358  con2biddc  812  nfalt  1515  alexim  1581  19.36-1  1608  ax11ev  1756  equs5or  1758  necon2bd  2313  necon2d  2314  necon1bbiddc  2318  necon2abiddc  2321  necon2bbiddc  2322  necon4idc  2324  necon4ddc  2327  necon1bddc  2332  spc2gv  2709  spc3gv  2711  mo2icl  2792  reupick  3281  prneimg  3613  invdisj  3831  trin  3938  ordsucss  4311  eqbrrdva  4594  elreldm  4649  elres  4735  xp11m  4856  ssrnres  4860  opelf  5167  dffo4  5431  dftpos3  6009  tfr1onlemaccex  6095  tfrcllemaccex  6108  nnaordex  6266  swoer  6300  map0g  6425  mapsn  6427  nneneq  6553  fnfi  6625  prarloclemlo  7032  genprndl  7059  genprndu  7060  cauappcvgprlemladdrl  7195  caucvgprlemladdrl  7216  caucvgsrlemoffres  7324  caucvgsr  7326  nntopi  7408  letr  7547  reapcotr  8051  apcotr  8060  mulext1  8065  lt2msq  8319  nneoor  8818  xrletr  9242  icoshft  9376  caucvgre  10379  absext  10461  rexico  10619  isummo  10737  gcdeq0  11050  bj-inf2vnlem2  11512
  Copyright terms: Public domain W3C validator