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-1 5  ax-2 6  ax-3 7  ax-mp 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