New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl6ib GIF version

Theorem syl6ib 217
 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 186 . 2 (χθ)
41, 3syl6 29 1 (φ → (ψθ))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177 This theorem is referenced by:  3imtr3g  260  exp4a  589  mtord  641  19.23hOLD  1820  ax12olem6  1932  cbvexd  2009  ax15  2021  2eu3  2286  exists2  2294  necon2bd  2565  necon2d  2566  necon4ad  2577  necon4d  2579  necon1bd  2584  spcimgft  2930  eqsbc3r  3103  reupick  3539  evenodddisj  4516  sfinltfin  4535  vfin1cltv  4547  dmcosseq  4973  iss  5000  xp11  5056  ssrnres  5059  opelf  5235  mapsn  6026
 Copyright terms: Public domain W3C validator