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

Theorem syl6ibr 218
Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded consequent with a definition. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl6ibr.1
syl6ibr.2
Assertion
Ref Expression
syl6ibr

Proof of Theorem syl6ibr
StepHypRef Expression
1 syl6ibr.1 . 2
2 syl6ibr.2 . . 3
32biimpri 197 . 2
41, 3syl6 29 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  3imtr4g  261  imp4a  572  3impexpbicom  1367  nic-ax  1438  nfimd  1808  equs5e  1888  euim  2254  mopick2  2271  2moswap  2279  2eu1  2284  necon3ad  2552  necon3d  2554  necon1d  2585  ralrimd  2702  spcimegf  2933  spcegf  2935  spcimedv  2938  spc2gv  2942  spc3gv  2944  rspcimedv  2957  eqsbc3r  3103  ra5  3130  tpid3g  3831  pwpw0  3855  sssn  3864  pwsnALT  3882  ssiun  4008  ssiun2  4009  spfininduct  4540  dmcosseq  4973  ssreseq  4997  ssrnres  5059  fnun  5189  f1oun  5304  fvopab3ig  5387  chfnrn  5399  dffo5  5424  fvclss  5462  fnoprabg  5585  ovigg  5596  leltctr  6212  spacind  6287  fnfrec  6320
  Copyright terms: Public domain W3C validator