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  773  nfalt  1467  alexim  1533  19.36-1  1560  ax11ev  1706  equs5or  1708  necon2bd  2257  necon2d  2258  necon1bbiddc  2262  necon2abiddc  2265  necon2bbiddc  2266  necon4idc  2268  necon4ddc  2271  necon1bddc  2276  spc2gv  2637  spc3gv  2639  mo2icl  2714  eqsbc3r  2813  reupick  3215  prneimg  3536  invdisj  3750  trin  3855  ordsucss  4196  eqbrrdva  4448  elreldm  4503  elres  4589  xp11m  4702  ssrnres  4706  opelf  5005  dffo4  5258  dftpos3  5818  tfr0  5878  nnaordex  6036  swoer  6070  prarloclemlo  6476  genprndl  6503  genprndu  6504  cauappcvgprlemladdrl  6628  letr  6878  reapcotr  7362  apcotr  7371  mulext1  7376  lt2msq  7613  nneoor  8096  xrletr  8474  icoshft  8608  bj-inf2vnlem2  9401
  Copyright terms: Public domain W3C validator