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

Theorem syl6ib 150
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 113 . 2 (χθ)
41, 3syl6 29 1 (φ → (ψθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3imtr3g  193  exp4a  348  con2biddc  762  nfalt  1448  alexim  1514  19.36-1  1541  ax11ev  1687  equs5or  1689  necon2bd  2237  necon2d  2238  necon1bbiddc  2242  necon2abiddc  2245  necon2bbiddc  2246  necon4idc  2248  necon4ddc  2251  necon1bddc  2256  spc2gv  2616  spc3gv  2618  mo2icl  2693  eqsbc3r  2792  reupick  3194  prneimg  3515  invdisj  3729  trin  3834  ordsucss  4176  eqbrrdva  4428  elreldm  4483  elres  4569  xp11m  4682  ssrnres  4686  opelf  4983  dffo4  5236  dftpos3  5795  frec0g  5898  nnaordex  6007  swoer  6041  prarloclemlo  6342  genprndl  6370  genprndu  6371  letr  6693  bj-inf2vnlem2  7328
  Copyright terms: Public domain W3C validator